proposition: Lemma pos_ord : forall m n, TPos m >>= TPos n -> Peano.ge m n.
proof: Proof. intros. inversion H; simpl in H0. lia. injection H0. lia. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)