proposition: Lemma tuto_subn_gt0 : forall m n, (0 < n - m) = (m < n).
proof: Proof. elim=> [|m IHm] [|n] //; exact: IHm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)