![[Previous]](prev.gif){kind=small}
![[Next]](next.gif){kind=small}
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)) ).
|
|
l'interface graphique PCoq |
|
|
|---|---|---|---|
affichage des formules mathématiques et logiques
|
|||
|
|