proposition: Lemma min_le_r: ∏ a b : (nat), min a b ≤ b.
proof: Proof. intros; unfold min; revert a. induction b as [| b IH]; destruct a ; try reflexivity. apply IH. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings