proposition: Lemma Key_2 : forall (i k k' j : nat) (ai ak ak' t : IR), 1 <= k -> k < i -> [0] [<=] ai -> [0] [<=] t -> ak[*] (t[*]p3m (S j)) [^]k[-]Halfeps [<=] ak'[*] (t[*]p3m (S j)) [^]k' -> ai[*] (t[*]p3m j) [^]i[-]eps [<=] ak[*] (t[*]p3m j) [^]k -> ai[*] (t[*]p3m (S j)) [^]i[-]eps [<=] ak'[*] (t[*]p3m (S j)) [^]k'.
proof: Proof. intros. apply Halfeps_trans with (ak[*] (t[*]p3m (S j)) [^]k). apply Key_1; auto. auto. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)