proposition: Lemma subn_if_gt T m n F (E : T) : (if m.+1 - n is m'.+1 then F m' else E) = (if n <= m then F (m - n) else E).
proof: Proof. by have [le_nm|/eqnP-> //] := leqP; rewrite -{1}(subnK le_nm) -addSn addnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring