fact: Definition lattice_for_gt_well_founded {T} {lt : T -> T -> bool} (gt_wf : well_founded (Basics.flip lt)) : well_founded (Basics.flip (lattice_for_lt lt)).
imports: Coq.PArith.BinPos Coq.PArith.Pnat Coq.Arith.Arith Coq.Classes.RelationClasses Coq.Classes.Morphisms Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common.Tactics.SplitInContext Fiat.Common.Notations