Theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits'

Modification history