proposition: Theorem lt_not_wf : ~ (well_founded T3lt).
proof: Proof. set f := (fix f i := if i is n.+1 then cons zero zero zero 0 (f n) else omega). case/not_decreasing; exists f; elim => //. by move => n fn; rewrite /f -/f T3lt_consE /= fn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)