Corrige' de 6.1

Premiere tactique:

On d\'eplie la def de born\'ee: le but devient:

$\exists m,M \in \rr, \forall x \in \rr, 
 m \le  \frac {x^2}{x^2 +1} \et 
\frac {x^2}{x^2 +1} \le M $.

On exhibe $m:=0$ puis M:=1$. Le but devient 

$\forall x \in \rr, 
 0 \le  \frac {x^2}{x^2 +1} \et 
\frac {x^2}{x^2 +1} \le 1 $.

On introduit $x$; le contexte contient donc le r\'eel $x$ 
et le nouveau but est 

$ 0 \le  \frac {x^2}{x^2 +1} \et 
\frac {x^2}{x^2 +1} \le 1 $.

Ici, on applique une tactique ``Casser et'' (il y a aussi 
une tactique ``casser ou'' que je n'ai pas non plus mise dans le cours 
virtuel mais vous savez les inventer) qui remplace ce but par les deux buts 
$ 0 \le  \frac {x^2}{x^2 +1}$, et $
\frac {x^2}{x^2 +1} \le 1 $.

Pour le premier, on applique une ressource qui dit

$\forall a,b  \in \rr, 
 0 \le a  \et 0 < b \imp   0 \le \frac {a}{b} $ aux arguments $a:=x^2$ 
et $b:= x^2+1$.
Ceci  g\'en\`ere deux nouveaux buts:


$0 \le x^2$ et $ 0 \le x^2+1 $.


Pour le premier, on applique une ressource qui dit

$\forall a  \in \rr, 
 0 \le a^2 $ avec $a:=x$. Ceci ne g\'en\`ere pas de nouveau but.


Pour le second, on applique une ressource qui dit



$\forall a,b  \in \rr, 
 0 \le a  \et 0 < b \imp   0 < a+b $ aux arguments $a:=x^2$ et $b:=1$.


Ceci  g\'en\`ere deux nouveaux buts:


$0 \le x^2$ et $ 0 < 1 $. On vient de d\'emontrer le premier, et le second est 
une ressource.

On passe \`a $
\frac {x^2}{x^2 +1} \le 1 $. 

Ici on applique une ressource qui dit:


$\forall a,b  \in \rr, 
 0 \le a  \et a < b \imp   \frac {a}{b} \le 1$ aux arguments 
$a:=x^2$ et $b:=x^2+1$.


Ceci  g\'en\`ere deux nouveaux buts:


$0 \le x^2$ et $ x^2 < x^2+1 $. On a d\'ej\`a prouv\'e le premier (dans le 
m\^eme contexte). Pour le second, on invoque une ressource qui dit 

$\forall a,b  \in \rr, 
 0  < b \imp   a < a+b$ avec $a:=x^2$ et $b:= 1$.



Ceci b\'en\`ere  un dernier but $0<1$ qui est une ressource.