proposition: Lemma add_le4 a b: b != zero -> a < a + b.
proof: Proof. move: (add_le1 a b); rewrite T3le_eqVlt. by case: (a<a+b); rewrite ? orbT // orbF => /eqP /add_le3 ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)