proposition: Lemma existence_representant_unitaire : forall A B : PO, A <> B -> exists C : PO, vec A C = representant_unitaire (vec A B).
proof: Proof. intros A B H; try assumption. elim existence_unitaire with (A := A) (B := B); [ intros C H0; try clear existence_unitaire; try exact H0 | auto ]. exists C. elim H0; intros H1 H2; elim H2; intros H3 H4; try clear H2 H0; try exact H4. apply def_representant_unitaire; auto. Qed.