Is there any support in mathcomp/ssreflect for classical logic

Question

For example, coq has in its standard library a Classical package with lemmas in classical logic such as ones that relate forall and exists (https://coq.inria.fr/library/Coq.Logic.Classical_Pred_Type.html).

My question is if there is any support like that in mathcomp or ssreflect itself. All I have found so far is a few definitions and lemmas in https://github.com/coq/stdlib2/blob/master/src/bool.v#L548

Thanks

user_1633770 · Answer

I don't think there is anything along those lines in the basic mathcomp libraries. The closest might be the classically operator in ssrbool, which mimics classical reasoning in intuitionistic logic. However, the experimental mathcomp analysis library assumes classical axioms and has results like the ones you mentioned (https://github.com/math-comp/analysis/blob/master/theories/boolp.v).