proposition: Lemma natminus1lthn (n : nat) : n > 0 -> n - 1 < n.
proof: Proof. intros n_gt_0. apply natminuslthn. - assumption. - reflexivity. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings