proposition: Lemma Zcompare_Eq_eq : forall n m : Z, (n ?= m) = Eq -> n = m.
proof: Proof. intros [ | p | p ] [ | q | q] E; simpl in E; reflexivity || solve [ inversion E ] || (f_equal; eapply Pcompare_Eq_eq; eauto). fold (p ?= q)%positive; destruct ((p ?= q)%positive); auto || inversion E. Defined.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm