proposition: Lemma SGe: (s <= t-2).
proof: Proof. unfold s. cut (2<= Nat.div2 t)%Z. lia. apply Zmult_le_reg_r with 2%Z; try lia. replace (Nat.div2 t*2)%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 (-1+(S ( Nat.double (Nat.div2 t))))%Z. 2: lia. rewrite <- Odd_double; auto with zarith. case (Zle_lt_or_eq 4 t); auto with zarith. intros I2; absurd (Nat.Odd t); auto. intros I3; apply Nat.Even_Odd_False with t; auto. replace t with (4) by auto with zarith. now exists 2. unfold Nat.double; rewrite inj_plus; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz