proposition: Lemma angles_et_colinearite : forall (A B C D E F G I : PO) (k1 k2 : R), A <> B :>PO -> C <> D :>PO -> E <> F :>PO -> G <> I :>PO -> vec E F = mult_PP k1 (vec A B) :>PP -> vec G I = mult_PP k2 (vec C D) :>PP -> double_AV (cons_AV (vec A B) (vec C D)) = double_AV (cons_AV (vec E F) (vec G I)) :>AV.
proof: Proof. intros A B C D E F G I k1 k2 H H0 H1 H2 H3 H4; try assumption. cut (k1 <> 0); intros. cut (k2 <> 0). intros H16; try assumption. elim existence_representant_vecteur with (A := A) (B := E) (C := F). intros J H6; try assumption. elim existence_representant_vecteur with (A := C) (B := G) (C := I). intros K H7; try assumption. rewrite <- H6 in H3. rewrite <- H7 in H4. cut (alignes A B J); intros. cut (A <> J); intros. cut (alignes C D K); intros. cut (C <> K); intros. rewrite (alignement_et_angles (A:=A) (B:=B) (C:=J) (D:=C) (E:=D) (F:=K)); auto. rewrite H6; rewrite H7; auto. apply distinct_produit_vecteur with (3 := H4); auto. apply colineaire_alignes with (1 := H4); auto. apply distinct_produit_vecteur with (3 := H3); auto. apply colineaire_alignes with (1 := H3); auto. red in |- *; intros; apply H2. apply conversion_PP with (a := 1) (b := 1); auto; try discrR. unfold vec in H4. RingPP2 H4. rewrite H6. RingPP. red in |- *; intros; apply H1. unfold vec in H3. apply conversion_PP with (a := 1) (b := 1); auto; try discrR. RingPP2 H3. rewrite H5. RingPP. Qed.