proposition: Lemma parallelogramme_non_concours : forall A B A1 B1 S : PO, ~ alignes A A1 B -> alignes A A1 S -> alignes B B1 S -> add_PP (cons 1 A) (cons (-1) A1) <> add_PP (cons 1 B) (cons (-1) B1).
proof: Proof. intros. contrapose H. assert (vec A1 A = vec B1 B). unfold vec in |- *. RingPP1 H2. RingPP. halignes H1 k. assert (A1 = A); auto with geo. apply vecteur_nul_conf. rewrite H3; rewrite H1; Ringvec. halignes H0 k0. apply colineaire_alignes with (k0 + - k). VReplace (vec A B) (add_PP (vec A S) (mult_PP (-1) (vec B S))). rewrite H5; rewrite H4. VReplace (vec B B1) (mult_PP (-1) (vec B1 B)). rewrite <- H3. Ringvec. Qed.