#===================================================
#
#  Examples for RQE based geometrical inequality proving - QEPCAD file [1]
#   Each example is given with their inputs for
#   QEPCAD for easy copy/pasting
#
#  Version 1.b - 17/04/20
#===================================================

#===================================================

#1: Bottema 1-1
[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\  (1+b+c)^2=m (b+ c+b c)].
assume[m>0].
finish

#2: Bottema 1-2
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (1+b^2+c^2) 4 (1+b+c)= m ((1+b+c)^3 +8 b c) ].
finish

#3: Bottema 1-3
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ m  (b+c-1) (1+c-b) (1+b-c)= 8 b c ].
finish

#4: Bottema 1-4
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ m b c=(b+1) (c+1) (b+c) ].
finish

#5: Bottema 1-5
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (1+b) (1+c) (b+c) = m (1^3+b^3+c^3) ].
assume[m>0].
finish

#6: Bottema 1-6
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (1 + b + c) (1^2 + b^2 + c^2) = m (1^3 + b^3 + c^3 + 3 b c) ].
assume[m>0].
finish

#7: Bottema 1-7
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (b + c - 1) + b^2 (1 + c - b) + c^2 (1 + b - c) = m 2 b c ].
assume[m>0].
finish

#8: Bottema 1-8
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ 8 (b c (b + c) + 1 c (1 + c) + 1 b (1 + b)) = m (b + c - 1) (1 + c - b) (1 + b - c) ].
assume[m>0].
finish

#9: Bottema 1-9
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ 1^3 (b + c - 1) + b^3 (1 + c - b) + c^3 (1 + b - c) = m b c (1 + b + c) ].
assume[m>0].
finish

#10: Bottema 1-11
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\  1^2 b (1-b)+b^2 c (b-c)+c^2 1 (c-1) = m].
finish

#11: Bottema 1-12
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (1+b+c)^3 (b+c-1) (1+c-b) (1+b-c)= 64 m (1 b c)^2].
assume[m>0].
finish

#12: Bottema 1-13-a1
(b,c,m,q)
3
(Eq)[q>0 /\ 2 q^2=(1-b)^2+(b-c)^2+(c-1)^2 /\ 1+b>c /\ 1+c>b /\ b+c>1 /\ m b c = 2 ((1/2)(1+b+c)-q) (1+b+c+q)^2].
assume[m>0].
proj-op(m,m,h)
finish

#13: Bottema 1-13-a2
(m,b,c)
1
(Eb)(Ec)[c - b - 1 < 0 /\ c - b + 1 > 0 /\ c + b - 1 > 0 /\ b c m + 2 c^3 - 3 b c^2 - 3 c^2 - 3 b^2 c - 15 b c - 3 c + 2 b^3 - 3 b^2 - 3 b + 2 < 0 /\ b^2 c^2 m^2 + 4 b c^4 m - 6 b^2 c^3 m - 6 b c^3 m - 6 b^3 c^2 m - 30 b^2 c^2 m - 6 b c^2 m + 4 b^4 c m - 6 b^3 c m - 6 b^2 c m + 4 b c m - 27 b^2 c^4 - 54 b c^4 - 27 c^4 + 54 b^3 c^3 + 108 b^2 c^3 + 108 b c^3 + 54 c^3 - 27 b^4 c^2 + 108 b^3 c^2 + 243 b^2 c^2 + 108 b c^2 - 27 c^2 - 54 b^4 c + 108 b^3 c + 108 b^2 c - 54 b c - 27 b^4 + 54 b^3 - 27 b^2 = 0].
assume[m>0].
finish

#14: Bottema 1-14
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\  m (1+b+c) b c = 2 (b^2 c^2+c^2+b^2)].
assume[m>0].
finish

#15: Bottema 1-15
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\  (1+b+c) ((1+c-b)(1+b-c)+(b+c-1)(1+b-c)+(b+c-1)(1+c-b)) = m (b+c-1) (1+b-c) (1+c-b)].
assume[m>0].
finish

#16: Bottema 1-16
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\  (c+1)(b+1)+b(b+c)(b+1)+c(b+c)(c+1) =m (b+c)(c+1)(b+1)].
assume[m>0].
finish

#17: Bottema 1-17
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (b+c+3)(b+1)(c+1)+(1+c+3b)(b+1)(b+c)+(1+b+3c)(c+1)(b+c)=2 m (b+c)(1+b)(1+c)].
assume[m>0].
finish

#18: Bottema 1-18
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (b-1)(c-1) + m b c=(c^2-c)+(b^2-b)].
assume[m>0].
finish

#19: Bottema 1-19
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\  (1^2+b^2+c^2) = m (1+b+c)^2].
assume[m>0].
finish

#20: Bottema 1-20-1
(b,x,y,z,u,c)
5
(Ec)[x>0 /\ y>0 /\ z>0 /\ u>0 /\ 2 x^2=1+b+c /\ 2 y^2=b+c-1 /\ 2 z^2=1+c-b /\ 2 u^2=1+b-c /\1+b>c /\ 1+c>b /\ b+c>1].
finish

#21: Bottema 1-20-2
(x,y,z,u,b)
4
(Eb)[x - 1 > 0 /\ y > 0 /\ y^2 - x^2 + 1 = 0 /\ z > 0 /\ z^2 - x^2 + b = 0 /\ u > 0 /\ u^2 + x^2 - b - 1 = 0].
finish

#22: Bottema 1-20-3
(m,x,y,z,u)
1
(Ex)(Ey)(Ez)(Eu)[ y+z+u = m x /\ x - 1 > 0 /\ y > 0 /\ y^2 - x^2 + 1 = 0 /\ z > 0 /\ u > 0 /\ u^2 + z^2 - 1 = 0].
finish

#23: Bottema 1-23
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (1+b+c)^3 = (m (b c (b+c)+c (c+1)+b (b+1))-3 b c)].
assume[m>0].
finish

#24: Bottema 1-24
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (b+1)(c+1)=m b c+(b+b^2)+(c+c^2)].
assume[m>0].
finish