proposition: Lemma Al_Kashi_sin_cos: forall (a b c : R), (a + b) + c = pi -> Rsqr (sin c) = (Rsqr (sin a) + Rsqr (sin b)) - ((2 * sin a) * sin b) * cos c.
proof: Proof. intros. RReplace ((Rsqr (sin a) + Rsqr (sin b)) - ((2 * sin a) * sin b) * cos c) (((Rsqr (sin a) * Rsqr (cos c) + Rsqr (sin b)) - ((2 * sin a) * sin b) * cos c) - Rsqr (sin a) * (Rsqr (cos c) - 1)). replace ((Rsqr (sin a) * Rsqr (cos c) + Rsqr (sin b)) - ((2 * sin a) * sin b) * cos c) with (Rsqr (sin a * cos c - sin b)). 2:unfold Rsqr; ring. rewrite <- (trigo_Pythagore c). RReplace (Rsqr (cos c) - (Rsqr (cos c) + Rsqr (sin c))) (- Rsqr (sin c)). elim pi_moins_x with ( x := a + c ); [intros H0 H1]. replace b with (pi + - (a + c)). rewrite H1. rewrite sin_som. RReplace (sin a * cos c - (sin a * cos c + sin c * cos a)) (- (sin c * cos a)). replace (Rsqr (- (sin c * cos a))) with (Rsqr (sin c) * Rsqr (cos a)). 2:unfold Rsqr; ring. RReplace (Rsqr (sin c) * Rsqr (cos a) - Rsqr (sin a) * - Rsqr (sin c)) (Rsqr (sin c) * (Rsqr (cos a) + Rsqr (sin a))). rewrite trigo_Pythagore. ring. rewrite <- H; ring. Qed.