proposition: Lemma Pcompare_Eq_eq : forall a b, Pcompare a b Eq = Eq -> a = b.
proof: Proof. intros a; induction a; intros b; destruct b; intros E; simpl in E; try solve [ inversion E | auto | f_equal; apply IHa; eauto ]. exfalso; eapply Pcompare_notEq_notEq; eauto. exfalso; eapply (proj1 (Pcompare_notEq_notEq _ _)); eauto. Defined.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm