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