proposition: Lemma T2subnn x: x - x = zero.
proof: Proof. by elim: x => // a _ b _ n c Hc /=; rewrite !T2ltnn ltnn eqxx Hc if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)