{D C l1 l2 p : ℝ} (hl1 : 0 < l1) (hl : l1 < l2) (hp : 0 < p) : richardson (D + C * l1 ^ (-p)) (D + C * l2 ^ (-p)) l1 l2 p = D

Initializing...

{D C l1 l2 p : ℝ} (hl1 : 0 < l1) (hl : l1 < l2) (hp : 0 < p) : richardson (D + C * l1 ^ (-p)) (D + C * l2 ^ (-p)) l1 l2 p = D · Prove2Me