proposition: Lemma produit_longueur_absolu_Sin2 : forall A B C : PO, A <> B -> A <> C -> B <> C -> distance A B * (distance A C * Rabs (Sin (cons_AV (vec A B) (vec A C)))) = distance C A * (distance C B * Rabs (Sin (cons_AV (vec C A) (vec C B)))).
proof: Proof. intros. replace (distance A B * (distance A C * Rabs (Sin (cons_AV (vec A B) (vec A C))))) with (Rabs (aire (vec A B) (vec A C))). rewrite <- aire_ordre_cycle2; auto. rewrite def_aire; auto. repeat rewrite Rabs_mult. rewrite Rabs_right; auto with geo. rewrite Rabs_right; auto with geo. rewrite def_aire; auto. repeat rewrite Rabs_mult. rewrite Rabs_right; auto with geo. rewrite Rabs_right; auto with geo. Qed.