proposition: Lemma Pcompare_notEq_notEq : forall a b, (Pcompare a b Lt <> Eq) /\ (Pcompare a b Gt <> Eq).
proof: Proof. intros a; induction a; intros b; destruct b; split; intros E; simpl in E; try solve [ inversion E | auto | eapply (proj1 (IHa _)); eauto | eapply (proj2 (IHa _)); eauto ]. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm