proposition: Lemma cos_02_uniq x y : 0 <= x <= 2 -> cos x = 0 -> 0 <= y <= 2 -> cos y = 0 -> x = y.
proof: Proof. wlog xLy : x y / x <= y => [H xB cx0 yB cy0|]. by case: (lerP x y) => [/H //| /ltW /H H1]; [exact|exact/esym/H1]. move=> /andP[x_ge0 x_le2] cx0 /andP[y_ge0 y_le2] cy0. case: (x =P y) => // /eqP xDy. have xLLs : x < y by rewrite le_eqVlt (negPf xDy) in xLy. have /(Rolle xLLs)[x1 _|x1|x1 x1I [_ x1D]] : cos x = cos y by rewrite cy0. - exact: derivable_cos. - by apply/continuous_subspaceT => ?; exact: continuous_cos. - have [_ /esym/eqP] := is_derive_cos x1; rewrite x1D oppr_eq0 => /eqP Hs. suff : 0 < sin x1 by rewrite Hs ltxx. apply/sin2_gt0/andP; split. + by rewrite (le_lt_trans x_ge0)// (itvP x1I). + by rewrite (lt_le_trans _ y_le2)// (itvP x1I). 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