proposition: Lemma min_le_iff : ∏ a b c : nat, (a ≤ min b c) <-> (a ≤ b ∧ a ≤ c).
proof: Proof. intros a b c; split. - intros le_a_mbc; split; eapply (istransnatleh le_a_mbc). + apply min_le_l. + apply min_le_r. - revert a c; induction b as [ | b' IH ]; intros a c [le_a_b le_a_c]. { intros; exact le_a_b. } destruct c as [ | c' ]. { exact le_a_c. } destruct a as [ | a' ]. { apply natleh0n. } apply IH. split; assumption. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings