proposition: Lemma law_cosines : forall x0 y0 x1 y1 x2 y2 ac:R, let a := dist_euc x1 y1 x0 y0 in let b := dist_euc x2 y2 x0 y0 in let c := dist_euc x2 y2 x1 y1 in a * c * cos ac = (x0 - x1) * (x2 - x1) + (y0 - y1) * (y2 - y1) -> Rsqr b = Rsqr c + Rsqr a - 2 * (a * c * cos ac).
proof: Proof. unfold dist_euc; intros; repeat rewrite Rsqr_sqrt; [ rewrite H; unfold Rsqr; ring | apply Rplus_le_le_0_compat | apply Rplus_le_le_0_compat | apply Rplus_le_le_0_compat ]; apply Rle_0_sqr. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt