proposition: Lemma positifColineaire_orient_r: forall (A B C M :PO), orient A B C -> positifColineaire A C M -> orient A B M.
proof: Proof. intros A B C M H [k [H0 [H1 H2]]]. unfold orient in *. rewrite H1. rewrite aire_colineaire_r. apply Rmult_gt_0_compat;auto. Qed.