proposition: Lemma ge_dec : forall x y, {ge x y}+{~ge x y}.
proof: Proof. intros x y. unfold ge, BigN.le. destruct (Z_le_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)