proposition: Lemma Chasles_diff : forall A B C D E F : PO, A <> B :>PO -> C <> D :>PO -> E <> F :>PO -> plus (cons_AV (vec A B) (vec C D)) (opp (cons_AV (vec A B) (vec E F))) = cons_AV (vec E F) (vec C D) :>AV.
proof: Proof. intros. rewrite def_opp; auto. rewrite plus_commutative; auto with geo. Qed.