proposition: Lemma gt_dec : forall x y, {gt x y}+{~gt x y}.
proof: Proof. intros. unfold gt, BigN.lt. destruct (Z_lt_dec (BigN.to_Z y) (BigN.to_Z x)). left. lia. right. lia. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)