Lemma min_le_iff : ∏ a b c : nat, (a ≤ min b c) <-> (a ≤ b ∧ a ≤ c). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.RigsAndRings.