proposition: Lemma alignement_et_angles : forall A B C D E F : PO, A <> B :>PO -> D <> E :>PO -> A <> C :>PO -> D <> F :>PO -> alignes A B C -> alignes D E F -> double_AV (cons_AV (vec A B) (vec D E)) = double_AV (cons_AV (vec A C) (vec D F)) :>AV.
proof: Proof. intros; unfold double_AV in |- *. rewrite angles_representants_unitaires; auto. rewrite angles_representants_unitaires; auto. elim existence_representant_unitaire with (A := D) (B := E); [ intros; try clear existence_representant_unitaire | auto ]. cut (D <> x); intros. elim existence_representant_unitaire with (A := A) (B := C); [ intros; try clear existence_representant_unitaire | auto ]. cut (A <> x0); intros. elim existence_representant_vecteur with (A := A) (B := D) (C := x); intros. cut (A <> x1); intros. elim alignes_representant_unitaire with (A := A) (B := B) (C := C); [ intros; try clear alignes_representant_unitaire; auto | intros; auto | auto | auto | auto ]. elim alignes_representant_unitaire with (A := D) (B := E) (C := F); [ intros; try clear alignes_representant_unitaire; auto | intros; auto | auto | auto | auto ]. rewrite H12; rewrite H11; auto. rewrite H12; rewrite H11; auto. replace (mult_PP (-1) (representant_unitaire (vec D E))) with (vec x D). rewrite <- H7; rewrite <- H5. replace (cons_AV (vec A x0) (vec x D)) with (plus (cons_AV (vec A x0) (vec D x)) (cons_AV (vec D x) (vec x D))). rewrite <- angle_plat; auto. rewrite <- H9. mesure A x0 A x1. replace (x2 + pi + (x2 + pi)) with (x2 + x2 + deuxpi); auto. rewrite (add_mes_compatible (x2 + x2) deuxpi). rewrite pi_plus_pi. rewrite <- add_mes_compatible. replace (x2 + x2 + 0) with (x2 + x2); auto. ring. unfold deuxpi; ring. rewrite Chasles; auto. rewrite <- H5. Ringvec. elim alignes_representant_unitaire with (A := D) (B := E) (C := F); [ intros; try clear alignes_representant_unitaire; auto | intros; auto | auto | auto | auto ]. replace (representant_unitaire (vec A B)) with (vec x0 A). rewrite <- H7; rewrite <- H12; rewrite <- H5; rewrite <- H9. replace (cons_AV (vec x0 A) (vec A x1)) with (plus (cons_AV (vec x0 A) (vec A x0)) (cons_AV (vec A x0) (vec A x1))). mesure A x0 A x1. rewrite <- angle_plat; auto. rewrite <- add_mes_compatible. rewrite <- add_mes_compatible. replace (pi + x2 + (pi + x2)) with (x2 + x2 + deuxpi); auto. rewrite (add_mes_compatible (x2 + x2) deuxpi). rewrite pi_plus_pi. rewrite <- add_mes_compatible. replace (x2 + x2 + 0) with (x2 + x2); auto. ring. unfold deuxpi; ring. rewrite Chasles; auto. replace (vec x0 A) with (mult_PP (-1) (representant_unitaire (vec A C))); auto. rewrite H11. Ringvec. rewrite <- H7. Ringvec. replace (representant_unitaire (vec A B)) with (vec x0 A). rewrite H12; auto. replace (mult_PP (-1) (representant_unitaire (vec D E))) with (vec x1 A). rewrite <- H7; rewrite <- H5; rewrite <- H9. replace (cons_AV (vec x0 A) (vec A x1)) with (plus (cons_AV (vec x0 A) (vec A x0)) (cons_AV (vec A x0) (vec A x1))). mesure A x0 A x1. rewrite <- angle_plat; auto. rewrite <- add_mes_compatible. replace (cons_AV (vec A x0) (vec x1 A)) with (plus (cons_AV (vec A x0) (vec A x1)) (cons_AV (vec A x1) (vec x1 A))). rewrite <- angle_plat; auto. rewrite <- H13. repeat rewrite <- add_mes_compatible. replace (pi + x2 + (pi + x2)) with (x2 + x2 + (pi + pi)); auto. replace (x2 + x2 + (pi + pi)) with (x2 + pi + (x2 + pi)); auto. unfold deuxpi; ring. ring. rewrite Chasles; auto. rewrite Chasles; auto. VReplace (vec x1 A) (mult_PP (-1) (vec A x1)); auto. rewrite H9; rewrite H5; auto. VReplace (vec x0 A) (mult_PP (-1) (vec A x0)). rewrite H7; rewrite H11. Ringvec. unfold not in |- *; intros; apply H6. apply conversion_PP with (a := 1) (b := 1); auto with real. cut (vec D x = vec A x1); intros. RingPP2 H11. rewrite H10. Ringvec. rewrite H9; auto. apply distance_non_nulle. elim def_representant_unitaire2 with (A := A) (B := C) (C := x0); [ intros; elim H9; intros H22 H23; rewrite H22; try discrR | auto | auto ]. apply distance_non_nulle. elim def_representant_unitaire2 with (A := D) (B := E) (C := x); [ intros; elim H7; intros H22 H23; rewrite H22; try discrR | auto | auto ]. Qed.