l'interface graphique
PCoq
affichage des formules mathématiques et logiques
Lemma paralleles_vecteur :
(A, B, C, D : PO) ~( A == B ) -> ~( C == D ) ->
(paralleles (droite A B) (droite C D)) ->
(exT ? [k : R] (vec A B) == (mult_PP k (vec C D)) ).
JFLA 2004 F. GUILHOT