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