proposition: Lemma unite_aire : aire (vec O I) (vec O J) = 1.
proof: Proof. intros. deroule_OIJ. rewrite def_aire; 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.