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