Lemma min_eq_a_or_eq_b : ∏ a b : (nat), coprod (min a b = a) (min a b = b). 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.
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.