proposition: Lemma eqf2D a b c : f (a + b) = f a + b -> c <= b -> f (a + c) = f a + c.
proof: Proof. elim: c => [|c IH fabE cLb]; first by by rewrite !addn0. have facE : f (a + c) = f a + c by apply: IH => //; apply: ltnW. apply/eqP; rewrite eqn_leq leqfD andbT. apply: leqf2D (_ : _ <= _ + (b - c.+1)). by do 2 rewrite -addnA (subnKC cLb) ?fabE. Qed.
imports: mathcomp(all_ssreflect)