proposition: Lemma ge_peano : ge = Peano.ge.
proof: Proof. Proof using. extens. rew_to_le. rewrite le_peano. unfold inverse. intros. lia. Qed.
imports: Coq.Arith.Arith Coq.micromega.Lia TLC(LibTactics LibReflect LibBool LibOperation LibRelation LibOrder)