Let .. Qed should produce an opaque subproof instead of doing clearbody

[SkySkimmer]

ie translate Let foo : T. tacs. Qed. into Lemma foo_subproof : T. tacs. Qed. Let foo := foo_subproof. (but keeping the implicits etc straight)

This would break compatibility, we can introduce an option Let Qed Is Asbtract. The warning on Let Qed would only happen when the option is off. Then we can set the option default on and deprecate the option, and eventually remove it.

cf #17544 (with that PR we may also auto clearbody on top as there is not much point keeping foo := foo_subproof in the proof context).