proposition: Lemma ge_def : ge = (fun _2249 : nat => fun _2250 : nat => le _2250 _2249).
proof: Proof. apply fun_ext; intro x. apply fun_ext; intro y. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat