proposition: Lemma Peq_ok P P' : (P ?== P') = true -> P === P'.
proof: Proof. unfold Pequiv. revert P';induction P as [|p P IHP|P2 IHP1 p P3 IHP2]; intros P';destruct P' as [|p0 P'|P'1 p0 P'2];simpl; intros H l; try easy. - now apply (morph_eq CRmorph). - destruct (Pos.compare_spec p p0); [ subst | easy | easy ]. now rewrite IHP. - specialize (IHP1 P'1); specialize (IHP2 P'2). destruct (Pos.compare_spec p p0); [ subst | easy | easy ]. destruct (P2 ?== P'1); [|easy]. rewrite H in *. now rewrite IHP1, IHP2. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory