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

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

#1: RightTriangle-Bottema1.1a//IsoBottema1p1g
#1: sensitive to varorder (4-1) mforbidden: v8,v10,v9,v7
[]
(m,v10,v9,v8,v7)
1
(Ev10)(Ev9)(Ev8)(Ev7)[m>0 /\ v9>0 /\ v10>0 /\ v10^2+1+v9^2+2v10+2v9 v10+2v9-m(v9+v10+v9 v10)=0 
/\ -v7^2-v8^2+v7=0 /\ -v10^2+v7^2+v8^2-2v7+1=0 /\ v7^2+v8^2-v9^2=0].
finish

#2: RightTriangle-Bottema 1.1b//IsoBottema1p1h
#2: sensitive to varorder (3-1) qdangereous v8v9v10 and v8v10v9 (120-150qs)
(m,v10,v9,v8)
1
(Ev10)(Ev9)(Ev8)[m>0 /\ v9>0 /\ v10>0 /\  v10^2+1+v9^2+2v9+2v10+2 v9 v10-m(v9+v10+v9 v10)=0 
/\ v8^2-v9^2+1=0 /\ -v10^2+v8^2=0].
finish

#3: RightTriangle-Bottema1.19a//IsoBottema1p19g
#3: sensitive to varorder (4-1) mdangereous: v8,v10,v9,v7
[]
(m,v10,v9,v8,v7)
1
(Ev10)(Ev9)(Ev8)(Ev7)[m>0 /\ v9>0 /\ v10>0 /\ v10^2+1+v9^2-m(v10^2+1+v9^2+2v10+2v9 v10+2v9)=0 
/\ -v7^2-v8^2+v7=0 /\ -v10^2+v7^2+v8^2-2v7+1=0 /\ v7^2+v8^2-v9^2=0].
finish



#4: RightTriangle-Bottema 1.19b//IsoBottema1p19h
#4: sensitive to varorder (3-1) qdangereous v8v9v10 and v8v10v9 (to-293qs)
(m,v10,v9,v8)
1
(Ev10)(Ev9)(Ev8)[m>0 /\ v9>0 /\ v10>0 /\  v10^2+1+v9^2-m(v10^2+1+v9^2+2v9+2v10+2 v9 v10)=0 
/\ v8^2-v9^2+1=0 /\ -v10^2+v8^2=0].
finish