proposition: Lemma sin_pihalf : sin (pi / 2) = 1.
proof: Proof. have := cos2Dsin2 (pi / 2); rewrite cos_pihalf expr0n add0r. rewrite -[in X in _ = X -> _](expr1n _ 2%N) => /eqP; rewrite -subr_eq0 subr_sqr. rewrite mulf_eq0=> /orP[|]; first by rewrite subr_eq0=> /eqP. rewrite addr_eq0 => /eqP spi21; have /sin2_gt0: 0 < pi / 2 < 2. by rewrite pihalf_lt2 andbT (lt_le_trans _ pihalf_ge1). by rewrite spi21 ltr0N1. 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