630 B
630 B
Теорема о параллелограмме
Ссылка на видеоразбор
Код из сайта
START_INTERACTIVE;;
(grobner_decide ** originate)
<<is_midpoint(m,a,c) /\ perpendicular(a,c,m,b)
==> lengths_eq(a,b,b,c)>>;;
#Parallelogram theorem
grobner_decide ** originate)
<<parallel(a,b,d,c) /\ parallel(a,d,b,c) /\
is_intersection(e,a,c,b,d)
==> lengths_eq(a,e,e,c)>>;;
(grobner_decide ** originate)
<<parallel(a,b,d,c) /\ parallel(a,d,b,c) /\
is_intersection(e,a,c,b,d) /\ ~collinear(a,b,c)
==> lengths_eq(a,e,e,c)>>;;
END_INTERACTIVE;;