proposition: Lemma cas_degenere_alignes1 : forall A B C : PO, A <> C -> ~ alignes1 A A C.
proof: Proof. unfold alignes1 in |- *; intros. unfold not in |- *; intros. elim H0; intros k H1; try clear H0; try exact H1. apply H. apply conversion_PP with (a := k + (1 + - k)) (b := 1); auto. rewrite H1; RingPP. RReplace (k + (1 + - k)) 1. discrR. ring. Qed.