def c14

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqn.bend:22

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

22def c14(+S: Nat) -> {Nat.mul(S, 14n) == Nat.add(Nat.add(S, S), Nat.mul(S, 12n)) : Nat}:
23  Equal.trans(Nat, Nat.mul(S, 14n), Nat.mul(14n, S), Nat.add(Nat.add(S, S), Nat.mul(S, 12n)), NA.mul_comm(S, 14n), Equal.trans(Nat, Nat.mul(14n, S), Nat.add(S, Nat.add(S, Nat.mul(12n, S))), Nat.add(Nat.add(S, S), Nat.mul(S, 12n)), {==}, Equal.trans(Nat, Nat.add(S, Nat.add(S, Nat.mul(12n, S))), Nat.add(Nat.add(S, S), Nat.mul(12n, S)), Nat.add(Nat.add(S, S), Nat.mul(S, 12n)), Equal.sym(Nat, Nat.add(Nat.add(S, S), Nat.mul(12n, S)), Nat.add(S, Nat.add(S, Nat.mul(12n, S))), NA.add_assoc(S, S, Nat.mul(12n, S))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(S, S), z), Nat.mul(12n, S), Nat.mul(S, 12n), NA.mul_comm(12n, S)))))