proposition: Lemma leqf2D a b c : f (a + c) <= b + c -> f a <= b.
proof: Proof. elim: c => [|c IH fLb]; first by rewrite !addn0. apply: IH. by rewrite -ltnS -addnS (leq_trans _ fLb) // monof addnS. Qed.
imports: mathcomp(all_ssreflect)