// ========
// Show "if a|b and a|c then a|(b+c)":
// ========

// === Types: ===
// Introduce type 'natural number':
TYPE nat

// === Declarations: ===
LET divides < nat nat (notation = _|_)
LET plus    : nat nat -> nat (prior = 5, notation = _+_)
LET mul     : nat nat -> nat (prior = 6, notation = _*_)

// === Definitions: ===
// Define relation 'divides':
RDEF div (PARAMS n e nat, t e nat)(VARS q e nat)
          t|n :<=> EXISTS q : t*q = n

// === Rewrite-rules: ===
// Rewrite-rule for distributivity on 'mul' and 'plus':
RR distr (PARAMS x e nat, y e nat, z e nat)
           x*(y+z) --> x*y+x*z

// === Main goal: ===
GOAL (VARS a e nat, b e nat, c e nat)
       FORALL a : FORALL b : FORALL c :
         (a|b & a|c => a|(b+c))