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