proposition: Lemma ge_impl_fin_ge : forall m n, (m >= n)%Z -> Fin m >>= Fin n.
proof: Proof. intros. destruct (Z_le_lt_eq_dec n m). lia. left. simpl. lia. subst n. right. refl. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)