bonjour j'ai un DM à faire qui reprend ce qui a été dit sur ce site :
http://hal.archives-ouvertes.fr/docs...DF/RR-4362.pdf
que j'ai recopié ci-dessous, car je ne comprend pas bien leur façon de procéder, donc si quelqu'un pouvait me rééxpliquer la démarche ça serait tres gentil![]()
C’ est en étudiant la démonstration classique (donnée ci-dessous) du théorème de l’ angle inscrit et de
l’ angle au centre que l’ on a décidé des premiers objets à construire dans Coq et des axiomes de départ.
Démonstration : (N.B. : dans cette démonstration, on confond un angle orienté de vecteurs non nuls et
une de ses mesures, on remplace par exemple l’angle plat par p et l’angle nul par 0 ou 2p )
Les points A, B et M étant sur un cercle de centre O, les triangles OAM et OBM sont isocèles en
O et donc on a les égalités d’ angles orientés de vecteurs :
(MA,MO)= (AO, AM ) et (MO,MB)= (BM,BO).
En utilisant la relation de Chasles, on obtient (MA,MB)= (AO, AM )+ (BM,BO) et d’autre part
(OA,OB)= (OA,OM )+ (OM,OB)
En utilisant la somme des angles dans un triangle isocèle et en utilisant la propriété : pour tous
vecteurs non nuls u et v : on a (v,u)= -(u, v)
on obtient successivement (OA,OM )=p - 2(AM, AO)=p + 2(AO, AM )
et de même (OM,OB)=p - 2(BO,BM )=p + 2(BM, BO) . Et en sommant, il vient
(OA,OB)=p + 2(AO, AM )+p + 2(BM,BO) ce qui permet d’écrire
(OA,OB)= 2[(AO, AM )+ (BM,BO)]= 2(MA,MB). (
-----