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