fact: Axiom sig_not_dec : forall P : Prop, { ~~P } + { ~P }.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra