proposition: Lemma angles_droites_orthogonales : forall A B C D E F G I : PO, A <> B :>PO -> C <> D :>PO -> E <> F :>PO -> G <> I :>PO -> orthogonal (vec A B) (vec E F) -> orthogonal (vec C D) (vec G I) -> double_AV (cons_AV (vec E F) (vec G I)) = double_AV (cons_AV (vec A B) (vec C D)).
proof: Proof. unfold double_AV in |- *; intros. replace (cons_AV (vec A B) (vec C D)) with (plus (plus (cons_AV (vec A B) (vec E F)) (cons_AV (vec E F) (vec G I))) (cons_AV (vec G I) (vec C D))). mesure E F G I. mesure A B E F. mesure G I C D. replace (x0 + x + x1 + (x0 + x + x1)) with (x + x + (x0 + x0) + (x1 + x1)). symmetry in |- *. rewrite add_mes_compatible. rewrite add_mes_compatible. replace (image_angle (x0 + x0)) with (image_angle pi). replace (image_angle (x1 + x1)) with (image_angle pi). repeat rewrite <- add_mes_compatible. replace (x + x + pi + pi) with (x + x + deuxpi). rewrite add_mes_compatible; rewrite pi_plus_pi; rewrite <- add_mes_compatible. replace (x + x + 0) with (x + x); auto. ring. unfold deuxpi in |- *; ring. rewrite add_mes_compatible; rewrite H7. replace (plus (cons_AV (vec G I) (vec C D)) (cons_AV (vec G I) (vec C D))) with (double_AV (cons_AV (vec G I) (vec C D))); auto. rewrite orthogonal_angles; auto with geo. rewrite add_mes_compatible; rewrite H6. replace (plus (cons_AV (vec A B) (vec E F)) (cons_AV (vec A B) (vec E F))) with (double_AV (cons_AV (vec A B) (vec E F))); auto. rewrite orthogonal_angles; auto with geo. ring. rewrite Chasles; auto. rewrite Chasles; auto. Qed.