proposition: Lemma ge_gt_compat2 : forall x y z, x >> y -> y >>= z -> x >> z.
proof: Proof. unfold ge, gt. destruct x; destruct y; destruct z; simpl; intuition; try discr. inversion H1. subst. hyp. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)