proposition: Lemma alignes_representant_unitaire : forall A B C : PO, A <> B :>PO -> A <> C :>PO -> alignes A B C -> representant_unitaire (vec A B) = representant_unitaire (vec A C) \/ representant_unitaire (vec A C) = mult_PP (-1) (representant_unitaire (vec A B)).
proof: Proof. intros. halignes H1 k. elim Rtotal_order with (r1 := k) (r2 := 0); [ intros H3; try clear total_order | intros H3; elim H3; [ intros H4; try clear H3 total_order | intros H4; try clear H3 total_order; try exact H4 ] ]. right; try assumption. apply produit_negatif_representant_unitaire with k; auto. absurd (k = 0); auto. contrapose H0. apply (produit_zero_conf H2); auto. left; try assumption. apply produit_positif_representant_unitaire with k; auto. Qed.