proposition: Lemma opp_plus_plus_opp : forall A B C D E F G I : PO, A <> B :>PO -> C <> D :>PO -> E <> F :>PO -> G <> I :>PO -> opp (plus (cons_AV (vec A B) (vec C D)) (cons_AV (vec E F) (vec G I))) = plus (opp (cons_AV (vec A B) (vec C D))) (opp (cons_AV (vec E F) (vec G I))) :>AV.
proof: Proof. intros A B C D E F G I H H0 H1 H2; try assumption. mesure A B C D. mesure E F G I. replace (- (x + x0)) with (- x + - x0); auto. ring. Qed.