NEW URI

Proof Style English Proof Tree Sentence Format English Raw Lens Magnitude 1 2 3 4 5 10 25 max Lens Width 500 600 700 800 900 1000 1100 1200 1300 1400 1500 1600

Question:

• One-sided Elimination of a multiplicative inverse, part 2

Query

cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
    ( ~ equalish(a,additive_identity) )).

cnf(less_or_equal_3,negated_conjecture,
    ( less_or_equal(a,additive_inverse(multiplicative_identity)) )).

cnf(not_less_or_equal_4,negated_conjecture,
    ( ~ less_or_equal(additive_inverse(multiplicative_identity),multiplicative_inverse(a)) )).