proposition: Lemma ge_impl_pos_ge : forall m n, (m >= n)%nat -> TPos m >>= TPos n.
proof: Proof. intros. destruct (lt_eq_lt_dec m n) as [[m_n | m_n] | m_n]. lia. subst m. right. refl. left. trivial. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)