proposition: Lemma ge_gt_compat : forall x y z, x >= y -> y > z -> x > z.
proof: Proof. now intros x y z H1 H2; apply Nat.lt_le_trans with (1 := H2). Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)