#===================================================
#
#  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: IsoTriangle-Bottema1.1a//IsoBottema1p1c
#1: Nonsensitive to varorder 
[]
(m,v5,v6,v7)
1
(Ev5)(Ev6)(Ev7)[m>0 /\ v7>0 /\ (v7+2)^2-m(2v7+1)=0 /\ -v5^2-v6^2+1=0 
/\ -v7^2+v6^2+v5^2-2v5+1=0].
finish

#2: IsoTriangle-Bottema 1.1b//IsoBottema1p1d
#2: Nonsensitive to varorder
(m,v11,v10)
1
(Ev11)(Ev10)[m>0 /\ v11>0 /\ 4v11^2+1+4v11-m(v11^2+2v11)=0 /\ v10^2-v11^2+1/4=0].
finish

#3: IsoTriangle-Bottema1.19a//IsoBottema1p19c
#3: Nonsensitive to varorder 
[]
(m,v5,v6,v7)
1
(Ev5)(Ev6)(Ev7)[m>0 /\ v7>0 /\ v7^2+2-m(v7+2)^2=0 /\ -v5^2-v6^2+1=0 
/\ -v7^2+v6^2+v5^2-2v5+1=0].
finish

#4: IsoTriangle-Bottema 19.1b//IsoBottema1p19d
#4: Nonsensitive to varorder
(m,v11,v10)
1
(Ev11)(Ev10)[m>0 /\ v11>0 /\ 2v11^2+1-m(4v11^2+1+4v11)=0 /\ v10^2-v11^2+1/4=0].
finish