proposition: Lemma fin_ge_impl_ge : forall m n, Fin m >>= Fin n -> (m >= n)%Z.
proof: Proof. intros. destruct H. simpl in H. lia. injection H. intro. subst m. lia. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)