proposition: Lemma Abs_Cos_less_One : forall x, [0] [<] x -> x [<] Pi -> AbsIR (Cos x) [<] [1].
proof: Proof. intros. astepl (AbsIR (Sin (Pi [/]TwoNZ[-]x))). apply Abs_Sin_less_One. apply shift_less_minus; apply shift_plus_less'. unfold cg_minus in |- *; rstepr Pi; auto. apply shift_minus_less; apply shift_less_plus'. astepl ZeroR; auto. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac