proposition: Lemma minus_lt a b: a < b -> a - b = zero.
proof: Proof. by case: a b => // a b c n d // [] // a' b' c' n' d' /= ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)