#===================================================
#
#  Examples for RQE based geometrical inequality proving - Mma file [2]
#   Each example is given with their inputs for
#   Mma for easy copy/pasting
#   It meant to be as an input formula for the Mathematica function 
#   Resolve 
#  Version 2.0 - 17/04/20
#===================================================

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

#1: IsoTriangle-Bottema1.1a//IsoBottema1p1c
inputformb1p1c:=Exists[{v5,v6,v7}, m>0 \[And] v7>0 \[And] (v7+2)^2-m(2v7+1)==0 
\[And] -v5^2-v6^2+1==0 \[And] -v7^2+v6^2+v5^2-2v5+1 == 0]

#2: IsoTriangle-Bottema1.1b//IsoBottema1p1d
inputformb1p1d:=Exists[{v11,v10}, m>0 \[And] v11>0 \[And] 4v11^2+1+4v11-m(v11^2+2v11)==0 
\[And] v10^2-v11^2+1/4==0]

#3: IsoTriangle-Bottema1.19a//IsoBottema1p19c
inputformb1p19c:=Exists[{v5,v6,v7}, m>0 \[And] v7>0 \[And] v7^2+2-m(v7+2)^2==0 
\[And] -v5^2-v6^2+1==0 \[And] -v7^2+v6^2+v5^2-2v5+1 == 0]

#4: IsoTriangle-Bottema1.19b//IsoBottema1p19d
inputformb1p19d:=Exists[{v11,v10}, m>0 \[And] v11>0 \[And] 2v11^2+1-m(4v11^2+1+4v11)==0 
\[And] v10^2-v11^2+1/4==0]