proposition: Lemma sin_gt0_pihalf x : 0 < x < pi / 2 -> 0 < sin x.
proof: Proof. move=> /andP[x_gt0 xLpi]; apply: sin2_gt0; rewrite x_gt0 /=. by apply: lt_trans xLpi _; exact: pihalf_lt2. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) reals ereal nsatz_realtype signed topology normedtype landau sequences derive realfun exp