proposition: Lemma T3lcp0_pr x y: x < y -> (y==zero) = false.
proof: Proof. by move => xy; apply /negP => yz; move: xy; rewrite (eqP yz) T3ltn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)