proposition: Lemma tuto_subnKC : forall m n : nat, m <= n -> m + (n - m) = n.
proof: Proof. elim=> [|m IHm] [|n] // Hmn. Search _ (_.+1 + _ = _.+1). by rewrite addSn IHm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)