proposition: Lemma ge_gt_compat : forall x y z, x >>= y -> y >> z -> x >> z.
proof: Proof. Proof with simpl; intuition. intros. destruct y; destruct x; destruct z; auto... destruct H. simpl in *. lia. injection H. intros. subst... destruct H. contr. discr. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)