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