proposition: Lemma ge_gt_compat : forall x y z, x >>= y -> y >> z -> x >> z.
proof: Proof. intros. destruct y. destruct x. destruct z. unfold gt, ge in *. destruct H. simpl in H. lia. injection H. intro. subst z0. hyp. auto. exfalso. destruct H. auto. discr. exfalso. destruct H. auto. subst x. auto. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)