Théorème de Desargues
concernant les longueurs
lorsqu'on dit soit l la longueur du segment A B, il est nécessaire en Coq de prouver l'existence d'une telle longueur
pour un point A et une longueur l donnés, pour construire un point à distance l de A il faut en prouver l'existence
inversement il faut prouver en Coq que pour une longueur donnée ln, il existe deux points distant de ln
lorsqu'on dit soit a l'angle A B C, il faut prouver l'existence d'une tel angle
concernant les angles
Lemma ang_exists :
∀ A B C, A <> B -> C <> B -> ∃ a, ang a /\ a A B C
Lemma anga_exists :
∀ A B C, acute A B C -> ∃ a, anga a /\ a A B C
Lemma ang_const :
∀ a A B, ang a -> A <> B -> ∃ C, a A B C
Lemma ang_const_o :
∀ a A B P, ~Col A B P -> ang a -> not_null_ang a -> not_flat_ang a -> ∃ C, a A B C /\ one_side A B C P
Lemma ex_points_ang :
∀ a , ang a -> ∃ A B C, a A B C
les théorèmes prouvés pour les angles sont applicables aux angles aigus, moyennant la preuve qu'un angle aigu est un angle
afin de s'approcher de démonstrations faites à la main, on peut développer des tactiques servant à instancier les variables existentielles.
par exemple, étant donné A B P, trois points et a un angle non nul et non plat, la tactique Ltac nga_instance_o a A B P C permet de rajouter dans le contexte le point C, avec les hypothèse : a A B C et one_side A B P C
un dernier exemple
 |
en démontrant Pappus nous avons utilisé le fait que l'angle a = A O B = A' O B'
∀ O A A B B' a,
out O A A' -> out O B B' -> a A O B -> a A' O B' |