proposition: Lemma Zcompare_gt : forall (A:Type)(a a':A)(p q:Z), match (p?=q)%Z with Gt => a | _ => a' end = if Z_le_gt_dec p q then a' else a.
proof: Proof. intros. destruct Z_le_gt_dec as [H|H]. red in H. destruct (p?=q)%Z; auto; elim H; auto. rewrite H; auto. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia