proposition: Fact sinD_cosD x y : (sin (x + y) - (sin x * cos y + cos x * sin y)) ^+ 2 + (cos (x + y) - (cos x * cos y - sin x * sin y)) ^+ 2 = 0.
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 first. by rewrite /f cos0 sin0 !(mul1r, mul0r, add0r, subr0, subrr, expr0n). apply: is_derive_0_is_cst => {}x. by apply: trigger_derive; rewrite /GRing.scale /=; nsatz. 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