proposition: Lemma conversion_PP : forall (a b : R) (A B : PO), cons a A = cons b B :>PP -> a <> 0 :>R -> a = b :>R -> A = B :>PO.
proof: Proof. intros a b A B H H0 H1; try assumption. elim cons_inj with (a := a) (b := b) (A := A) (B := B); intros; try assumption. Qed.