proposition: Lemma if_add_eq m n : (if m < m + n then m else (m + n)%N) = m.
proof: Proof. case: n=> [|?]; first by rewrite addn0 ltnn. by rewrite ifT // -addn1 leq_add. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly matrix mxpoly) CoqEAL(hrel param refinements trivial_seq)