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