proposition: Lemma nat_lt0_succ m : (0 < m) = true -> exists m', m = m'+1.
proof: Proof. destruct m => //. move => _. exists m. by rewrite addn1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div)