proposition: Lemma Key_1 : forall (i k j : nat) (ai ak t : IR), 1 <= k -> k < i -> [0] [<=] ai -> [0] [<=] t -> ai[*] (t[*]p3m j) [^]i[-]eps [<=] ak[*] (t[*]p3m j) [^]k -> ai[*] (t[*]p3m (S j)) [^]i[-]Halfeps [<=] ak[*] (t[*]p3m (S j)) [^]k.
proof: Proof. intros i k j ai ak t H H0 H1 H2 H3. apply leEq_transitive with (p3m k[*] (ai[*] (t[*]p3m j) [^]i) [-]p3m k[*]eps). apply minus_resp_leEq_both. astepl (p3m i[*] (ai[*] (t[*]p3m j) [^]i)). apply mult_resp_leEq_rht. apply less_leEq. apply p3m_mon; auto. astepl (ai[*][0]). apply mult_resp_leEq_lft; auto. apply nexp_resp_nonneg. apply mult_resp_nonneg; auto. apply less_leEq; apply p3m_pos. apply Key_1b; auto. astepl (p3m k[*] (ai[*] (t[*]p3m j) [^]i[-]eps)). astepr (p3m k[*] (ak[*] (t[*]p3m j) [^]k)). apply mult_resp_leEq_lft; auto. apply less_leEq; apply p3m_pos. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)