proposition: Lemma invHalfPi_less_QuarterPi : [--] (Pi [/]TwoNZ) [<] Pi [/]FourNZ.
proof: Proof. apply less_transitive_unfolded with ZeroR. apply neg_invHalfPi. apply pos_QuarterPi. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos