proposition: Lemma pos_ge_impl_ge : forall m n, TPos m >>= TPos n -> (m >= n)%nat.
proof: Proof. intros. destruct H. auto with arith. injection H. intro. subst m. auto with arith. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)