proposition: Lemma min_eq_a_or_eq_b : ∏ a b : (nat), coprod (min a b = a) (min a b = b).
proof: Proof. intros a b. destruct (natleorle a b) as [le_a_b | le_b_a]. - apply inl. apply min_of_le; assumption. - apply inr. rewrite min_comm. apply min_of_le; assumption. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings