proposition: Lemma Triangle_equiv_expressions: let s:=((a+b+c)/2) in sqrt (s*(s-a)*(s-b)*(s-c)) = /4*sqrt ((a+(b+c))*(a+(b-c))*(c+(a-b))*(c-(a-b))).
proof: Proof. intros s. assert (0 <= /4). assert (0 < 2). apply Rle_lt_0_plus_1; apply Rlt_le; exact Rlt_0_1. left; apply Rinv_0_lt_compat. now repeat apply Rmult_lt_0_compat. assert (0 <= /16). apply Rle_trans with (/4*/4). now apply Rmult_le_pos. right; field. replace (/4) with (sqrt (/16)). rewrite <- sqrt_mult_alt. apply f_equal. unfold s; field. exact H0. apply sqrt_lem_1. exact H0. exact H. field. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)