proposition: Lemma orient_4point: forall (A B C D : PO), orient A B D -> orient B C D -> orient C A D -> orient A B C.
proof: Proof. intros A B C D H0 H1 H2. unfold orient in *. rewrite aire_ordre_cycle2 in H2. assert (H4:aire (vec A D) (vec B A) >0). rewrite aire_anti_symetrique. VReplace (vec B A) (mult_PP (-1) (vec A B)). rewrite aire_colineaire_l;lra. assert (H5: aire (vec A D) (vec B C) >0). rewrite <-(@Chasles_vec B A C). rewrite aire_distrib_l;lra. assert (H6 : aire (vec D B)(vec B C)>0). rewrite aire_anti_symetrique. VReplace (vec D B) (mult_PP (-1) (vec B D)). rewrite aire_colineaire_r;lra. assert (H7: aire (vec A B) (vec B C) >0). rewrite <-(@Chasles_vec A D B). rewrite aire_distrib_r;lra. rewrite <-(@Chasles_vec A B C ). rewrite aire_distrib_l. rewrite aire_ABAB;lra. Qed.