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). (
-----