proposition: Lemma norm_cos_eq1 x : (`|cos x| == 1) = (sin x == 0).
proof: Proof. rewrite -sqrf_eq0 -sqrp_eq1 // -normrX ger0_norm ?exprn_even_ge0 //. by rewrite [X in _ = (X == _)]sin2cos2 subr_eq0 eq_sym. 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