proposition: Lemma anglesEgaux_orient : forall (A B C M N P : PO), orient A B C -> M<>N -> M <>P-> cons_AV (vec M N) (vec M P) = cons_AV (vec A B ) ( vec A C)-> orient M N P.
proof: Proof. intros A B C M N P H H0 H1 H2. generalize H;intros H3. unfold orient in H3. unfold orient . rewrite def_aire in *;deroule_orient H;auto. elim (@distance_pos A B );intros H11 ; [idtac|elim (@distincts_dist_non_nulle A B H6);auto]. elim (@distance_pos A C );intros H12 ; [idtac|elim (@distincts_dist_non_nulle A C H8);auto]. elim (@distance_pos M N );intros H13 ; [idtac|elim (@distincts_dist_non_nulle M N H0);auto]. elim (@distance_pos M P );intros H14 ; [idtac|elim (@distincts_dist_non_nulle M P H1);auto]. rewrite H2. apply Rmult_gt_0_compat;auto. apply Rmult_gt_0_compat;auto. replace 0 with (distance A B *0) in H3;auto with real. apply orient_SinusPositif;auto. Qed.