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