proposition: Lemma parallelepipede_parallelogramme : forall A B C D E F G H : PO, parallelepipede A B C D E F G H -> vec F G = vec A D.
proof: Proof. unfold parallelepipede in |- *; intros A B C D E F G H' H. elim H; intros H0 H1; elim H1; intros H2 H3; try clear H1 H; try exact H3. elim H0; intros H H1; try clear H0; try exact H1. rewrite <- H3. apply egalite_vecteur. VReplace (vec F E) (mult_PP (-1) (vec E F)). rewrite <- H2. Ringvec. Qed.