proposition: Lemma SLe: (2 <= s).
proof: Proof. unfold s; auto with zarith. assert (2<= t-Nat.div2 t)%Z; auto with zarith. apply Zmult_le_reg_r with 2%Z; try lia. replace ((t-Nat.div2 t)*2)%Z with (2*t-2*Nat.div2 t)%Z by ring. replace (2*Nat.div2 t)%Z with (Z_of_nat (Nat.double (Nat.div2 t))). case (Nat.Even_or_Odd t); intros I. rewrite <- Even_double by easy. lia. apply Z.le_trans with (2*t+1-(S ( Nat.double (Nat.div2 t))))%Z; try lia. rewrite <- Odd_double by easy. lia. unfold Nat.double; rewrite inj_plus; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz