proposition: Lemma EntreDeuxVec_sym : forall (A B C M N :PO), vecEntreDeuxVec A B C M -> A<>N-> cons_AV ( vec A B) (vec A M) = cons_AV (vec A N) (vec A C) -> vecEntreDeuxVec A B C N.
proof: Proof. intros A B C M N H H0 H1. unfold vecEntreDeuxVec in *. assert (H2: A<>B /\ A<>C /\ A<>M). elim H;intros [H3[H4 H5]]; deroule_orient H3;deroule_orient H5;repeat split;auto. destruct H2 as [H2 [H3 H4]]. assert (H5: cons_AV (vec A B)(vec A N) = cons_AV (vec A M) (vec A C)). rewrite <-(@Chasles A B A M A N);auto. rewrite H1. rewrite plus_commutative. rewrite ->(@Chasles A M A N A C);auto. elim H;intros [H6[H7 H8]]. left. split;auto. split;auto. apply (@anglesEgaux_orient A M C);auto. apply (@anglesEgaux_orient A B M);auto. right. split;auto. split;auto. apply (@anglesEgaux_orient A M B);auto. apply permute_angles;auto. apply (@anglesEgaux_orient A C M);auto . apply permute_angles;auto. Qed.