proposition: Lemma negatifColineaire_orient_l: forall (A B C M :PO), orient A B C -> negatifColineaire A B M -> orient A C M.
proof: Proof. intros A B C M H [k [H0 [H1 H2]]]. unfold orient in *. rewrite H1. rewrite aire_colineaire_r. rewrite aire_anti_symetrique. rewrite Ropp_mult_distr_r_reverse. rewrite <- Ropp_mult_distr_l_reverse. apply Rmult_gt_0_compat;auto with real. Qed.