proposition: Lemma double_opp : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> double_AV (opp (cons_AV (vec A B) (vec C D))) = opp (double_AV (cons_AV (vec A B) (vec C D))) :>AV.
proof: Proof. unfold double_AV in |- *; intros. rewrite <- opp_plus_plus_opp; auto. Qed.