proposition: Lemma affixe_vec_AB_affixes : forall A B : PO, affixe_vec (vec A B) = Cplus (affixe B) (Copp (affixe A)).
proof: Proof. intros. elim existence_affixe_point with (M := A); intros a H; try exact H. elim existence_affixe_point with (M := B); intros b; intros. symmetry in |- *; rewrite <- H; rewrite <- H0. apply affixe_vec_AB; auto. Qed.