proposition: Lemma gt_def : gt = (fun _2261 : nat => fun _2262 : nat => lt _2262 _2261).
proof: Proof. apply fun_ext; intro x. apply fun_ext; intro y. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat