proposition: Lemma alignes_imageZeroPi: forall A B C : PO, A<>B->A<>C-> alignes A B C -> (cons_AV(vec A B)(vec A C) = image_angle 0) \/(cons_AV(vec A B)(vec A C) = image_angle pi).
proof: Proof. intros A B C H H0 H1. halignes H1 k. elim (Rtotal_order k 0);intros. right. rewrite ->(@angle_produit_negatif_r k A B C A B);auto. rewrite <-angle_nul;auto . rewrite plus_commutative with (a :=image_angle 0)(b:=image_angle pi);auto with geo. elim H3;intro H4. rewrite H4 in H2. rewrite (@produit_zero_conf k A C A B) in H0;auto. elim H0;auto. rewrite H4;assumption. left. rewrite (@angle_produit_positif_r k A B C A B );auto. rewrite <-angle_nul;auto . Qed.