An exact proof term for the current goal is (andEL (a ∈ R) (b ∈ R) (andEL (a ∈ R ∧ b ∈ R) (¬ (Rlt b a)) H)).