proposition: Lemma leq_sub_sub a b c : ((a - b) - (c - b)) <= a - c.
proof: Proof. have [aLb|bLa] := leqP b a; last first. rewrite (_ : a - _ = 0) ?sub0n //. by apply/eqP; rewrite subn_eq0 ltnW. have [cLb|bLc] := leqP c b; last first. by rewrite subnBA ?subnK // ltnW. rewrite (_ : c - _ = 0); last by apply/eqP; rewrite subn_eq0. by rewrite subn0 leq_sub2l. Qed.
imports: mathcomp(all_ssreflect)