proposition: Lemma bounded_has_maximal_nat : @bounded_has_minimal nat (inverse le).
proof: Proof. Proof using. intros P [ y ? ] [ x h ]. assert (y <= x). { forwards: h. eauto. eauto. } assert (self_inverse: forall i, i <= x -> (x - (x - i))%nat = i). intros. nat_math. forwards [ z [ ? hz ]]: (@bounded_has_minimal_nat (fun i => P (x - i)%nat)). { exists (x - y)%nat. rewrite self_inverse by eauto. eauto. } { eauto using admits_lower_bound_nat. } exists (x - z)%nat. clear dependent y. split; [ assumption | ]. intros y ?. assert (y <= x). { forwards: h. eauto. eauto. } forwards: hz (x - y)%nat. { rewrite self_inverse by eauto. eauto. } unfold inverse. nat_math. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation LibOrder LibEpsilon) TLC(LibNat)