proposition: Lemma leq_sub_add b a c : a - c <= (a - b) + (b - c).
proof: Proof. rewrite leq_subLR addnC -addnA. have [/subnK->|H] := leqP c b. have [/subnK->//|H] := leqP b a. apply: leq_trans (ltnW H) _. by apply: leq_addl. have := ltnW H. rewrite -subn_eq0 => /eqP->. rewrite addnC -leq_subLR. by apply: leq_sub2l; apply: ltnW. Qed.
imports: mathcomp(all_ssreflect)