Conservative definition
Parameters: ab, ac, db, dc, L
∀ x. ∀ y. S x ≤ L → S y ≤ S (S x · ac) ∧ (∃ z. ab = z · S (S x · ac) + y) → S (x · y) ≤ S (S x · dc) ∧ (∃ z. db = z · S (S x · dc) + x · y)Definition prerequisites
Theorem uses (notation, not proof premises)
CV007 · CV017 · CV021 · CV024 · CV026 · CV028 · CV029 · CV031 · CV034