theorem
proved
areaRateSlope_ne_neg_area_mul_ricciNull_of_nonzero_expansion
show as:
areaRateSlope_ne_neg_area_mul_ricciNull_of_nonzero_expansion