proposition: Lemma T3le_anti : antisymmetric T3le.
proof: Proof. move=> m n /andP [/orP []]; first by move /eqP ->. by move => mn /(T3lt_le_trans mn); rewrite T3ltnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)