P (lemma)
pair_equal_spec [in Corelib.Init.Datatypes]
pair_andP [in Corelib.ssr.ssrbool]
PartialOrder_inverse [in Corelib.Classes.RelationClasses]
PartialOrder_StrictOrder [in Corelib.Classes.CMorphisms]
PartialOrder_StrictOrder [in Corelib.Classes.Morphisms]
PartialOrder_inverse [in Corelib.Classes.CRelationClasses]
pcan_in_comp [in Corelib.ssr.ssrbool]
pcan_in_inj [in Corelib.ssr.ssrbool]
pcan_pcomp [in Corelib.ssr.ssrfun]
pcan_inj [in Corelib.ssr.ssrfun]
plus_Sn_m [in Corelib.Init.Peano]
plus_n_Sm [in Corelib.Init.Peano]
plus_O_n [in Corelib.Init.Peano]
plus_n_O [in Corelib.Init.Peano]
pointwise_pointwise [in Corelib.Classes.CMorphisms]
pointwise_pointwise [in Corelib.Classes.Morphisms]
pred_Sn [in Corelib.Init.Peano]
Prim2SF_inj [in Corelib.Floats.FloatAxioms]
prod_sigT_prod [in Corelib.Init.Specif]
proj1 [in Corelib.Init.Logic]
proj2 [in Corelib.Init.Logic]
proper_sym_arrow_iffT_2 [in Corelib.Classes.CMorphisms]
proper_sym_impl_iff_2 [in Corelib.Classes.CMorphisms]
proper_sym_arrow_iffT [in Corelib.Classes.CMorphisms]
proper_sym_impl_iff [in Corelib.Classes.CMorphisms]
proper_sym_flip_2 [in Corelib.Classes.CMorphisms]
proper_sym_flip [in Corelib.Classes.CMorphisms]
proper_normalizes_proper [in Corelib.Classes.CMorphisms]
proper_eq [in Corelib.Classes.CMorphisms]
proper_proper_proxy [in Corelib.Classes.CMorphisms]
proper_sym_impl_iff_2 [in Corelib.Classes.Morphisms]
proper_sym_impl_iff [in Corelib.Classes.Morphisms]
proper_sym_flip_2 [in Corelib.Classes.Morphisms]
proper_sym_flip [in Corelib.Classes.Morphisms]
proper_normalizes_proper [in Corelib.Classes.Morphisms]
proper_eq [in Corelib.Classes.Morphisms]
proper_proper_proxy [in Corelib.Classes.Morphisms]
prop_congr [in Corelib.ssr.ssrbool]