#ifdef TYPECHECK_SMT2__ #then
primplement
lemma_divisible_terms_to_sum {a, b} {d} () =
  let
    (* A proof by contradiction: I prove that the remainder
       ((a + b) mod d) has to be divisible. *)

    prval _ = prop_verify {a == d * (a / d)} ()
    prval _ = prop_verify {b == d * (b / d)} ()
    prval _ =
      prop_verify {a + b == (d * ((a + b) / d)) + ((a + b) mod d)} ()

    prval _ =
      prop_verify
        {(d * (a / d)) + (d * (b / d)) ==
            (d * ((a + b) / d)) + ((a + b) mod d)} ()
    prval _ =
      prop_verify
        {(a + b) mod d ==
            (d * (a / d)) + (d * (b / d)) - (d * ((a + b) / d))} ()
    prval _ =
      prop_verify
        {(a + b) mod d == d * ((a / d) + (b / d) - ((a + b) / d))} ()

    stadef k = (a / d) + (b / d) - ((a + b) / d)

    prval _ = lemma_divisible_factor_to_product {d, k} {d} ()
  in
    unit_p
  end
#endif (* TYPECHECK_SMT2__ *)