case S (m:nat).
by induction hypothesis we know (alpha2 m ≥ R1) (H).
we need to prove (alpha2 (S m) ≥ R1)
or equivalently (Rmult (alpha2 m) (alpha2 m) ≥ R1).letin xxx := (n ≤ n);
case S (m:nat).
by induction hypothesis we know (alpha2 m ≥ R1) (H).
we need to prove (alpha2 (S m) ≥ R1)
or equivalently (Rmult (alpha2 m) (alpha2 m) ≥ R1).letin xxx := (n ≤ n);