proposition: Lemma pihalf_02_cos_pihalf : 0 <= pi / 2 <= 2 /\ cos (pi / 2) = 0.
proof: Proof. have [x /andP[x1 x2] cs0] := cos_exists; rewrite pihalfE. case: xgetP => [_->[]//|/(_ x)/=]. by rewrite cs0 (le_trans _ x1)// x2 => /not_andP[]. 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