DefinitionsCache, czΞ±, dsΞ±, int, nat, rΞ±, ExBase, cast, cmp, eq, evalIntCast, evalNatCast, evalPos, toProd, ExProd, cast, cmp, coeff, eq, evalIntCast, evalInv, evalNatCast, evalPos, mkNNRat, mkNat, mkNegNNRat, mkNegNat, toSum, ExSum, cast, cmp, eq, evalIntCast, evalInv, evalNatCast, evalPos, ExtractCoeff, e', k, p, ve', Overlap, expr, proof, val, eval, evalAdd, evalAddOverlap, evalAtom, evalCast, evalDiv, evalInvAtom, evalMul, evalMulProd, evalMulβ, evalNSMul, evalNeg, evalNegProd, evalPow, evalPowAtom, evalPowNat, evalPowProd, evalPowProdAtom, evalPowβ, evalSub, evalZSMul, extractCoeff, instInhabitedResultOfSigmaQuoted, instInhabitedSigmaQuotedExBase, instInhabitedSigmaQuotedExProd, instInhabitedSigmaQuotedExSum, isAtomOrDerivable, mkCache, sβ, sβ€ | 75 |
Theoremsadd_congr, add_mul, add_overlap_pf, add_overlap_pf_zero, add_pf_add_gt, add_pf_add_lt, add_pf_add_overlap, add_pf_add_overlap_zero, add_pf_add_zero, add_pf_zero_add, add_pos_left, add_pos_right, atom_pf, atom_pf', cast_neg, cast_nnrat, cast_pos, cast_rat, cast_zero, coeff_mul, coeff_one, const_pos, div_congr, div_pf, intCast_add, intCast_mul, intCast_negOfNat_Int, intCast_zero, inv_add, inv_congr, inv_mul, inv_single, inv_zero, mul_add, mul_congr, mul_exp_pos, mul_one, mul_pf_left, mul_pf_right, mul_pow, mul_pp_pf_overlap, mul_zero, natCast_add, natCast_int, natCast_mul, natCast_nat, natCast_zero, neg_add, neg_congr, neg_mul, neg_one_mul, neg_zero, nsmul_congr, one_mul, one_pow, pow_add, pow_atom, pow_bit0, pow_bit1, pow_congr, pow_nat, pow_one, pow_one_cast, pow_prod_atom, pow_zero, single_pow, smul_eq_cast, smul_eq_intCast, smul_int, smul_nat, sub_congr, sub_pf, toProd_pf, zero_mul, zero_pow, zsmul_congr | 76 |