proposition: Lemma cos2Dsin2 x : (cos x) ^+ 2 + (sin x) ^+ 2 = 1.
proof: Proof. set v := LHS; pattern x in v; move: @v; set f := (X in let _ := X x in _) => /=. apply: (@eq_trans _ _ (f 0)); last by rewrite /f sin0 cos0 expr1n expr0n addr0. apply: is_derive_0_is_cst => {}x. apply: trigger_derive; rewrite /GRing.scale /=. by rewrite mulrN ![sin x * _]mulrC -opprD addrC subrr. 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