proposition: Lemma opp_unite_aire : aire (vec O J) (vec O I) = -1.
proof: Proof. intros. deroule_OIJ. rewrite def_aire; auto with geo. rewrite Sin_opp; auto with geo. rewrite (def_Sin (A:=O) (B:=I) (C:=J) (D:=J)); auto with geo. rewrite H1; rewrite H2; rewrite H3; ring. Qed.