Let z, w and v be given.
Assume Hz Hw Hv.
We prove the intermediate
claim Lwv:
HSNo (mult' w v).
An
exact proof term for the current goal is
HSNo_mul_HSNo w v Hw Hv.
We prove the intermediate
claim Lzw:
HSNo (mult' z w).
An
exact proof term for the current goal is
HSNo_mul_HSNo z w Hz Hw.
We prove the intermediate
claim Lzwv1:
HSNo (mult' z (mult' w v)).
An
exact proof term for the current goal is
HSNo_mul_HSNo z (mult' w v) Hz Lwv.
We prove the intermediate
claim Lzwv2:
HSNo (mult' (mult' z w) v).
An
exact proof term for the current goal is
HSNo_mul_HSNo (mult' z w) v Lzw Hv.
We prove the intermediate claim Lp0zR: CSNo (p0 z).
An
exact proof term for the current goal is
HSNo_proj0R z Hz.
We prove the intermediate claim Lp0wR: CSNo (p0 w).
An
exact proof term for the current goal is
HSNo_proj0R w Hw.
We prove the intermediate claim Lp0vR: CSNo (p0 v).
An
exact proof term for the current goal is
HSNo_proj0R v Hv.
We prove the intermediate claim Lp1zR: CSNo (p1 z).
An
exact proof term for the current goal is
HSNo_proj1R z Hz.
We prove the intermediate claim Lp1wR: CSNo (p1 w).
An
exact proof term for the current goal is
HSNo_proj1R w Hw.
We prove the intermediate claim Lp1vR: CSNo (p1 v).
An
exact proof term for the current goal is
HSNo_proj1R v Hv.
We prove the intermediate
claim L1:
CSNo (p0 w ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L2:
CSNo (p1 w ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L3:
CSNo (p1 v ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L4:
CSNo (p0 v ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L5:
CSNo (p0 v ' ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L6:
CSNo (p1 w ' ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L7:
CSNo (p1 w * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L8:
CSNo (p0 z * p0 w).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L9:
CSNo (p0 w * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L10:
CSNo (p0 w * p0 v).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L11:
CSNo (p1 v * p0 w).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L12:
CSNo ((p1 v * p0 w) ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L13:
CSNo ((p0 w * p0 v) ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L14:
CSNo (p1 z * p0 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L15:
CSNo (p0 z * p0 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L16:
CSNo (p0 v ' * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L17:
CSNo (p1 v * p1 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L18:
CSNo (p1 v ' * p1 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L19:
CSNo (p1 w ' * p1 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L20:
CSNo (p1 v ' * p1 w).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L21:
CSNo (p1 w * p0 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L22:
CSNo (p0 w ' * p1 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L23:
CSNo (p0 v ' ' * p1 w).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L24:
CSNo ((p1 w * p0 v ') ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L25:
CSNo ((p1 v ' * p1 w) ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L26:
CSNo (- p1 w ' * p1 z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L27:
CSNo (p0 w ' * p0 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L28:
CSNo (p0 v ' * p0 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L29:
CSNo (- p1 v ' * p1 w).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L30:
CSNo (p1 w ' * p1 w ' ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L31:
CSNo ((- p1 v ' * p1 w) ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L32:
CSNo (p1 v * p0 z * p0 w).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L33:
CSNo (p1 v * p0 w * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L34:
CSNo (p0 z * p0 w * p0 v).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L35:
CSNo (- (p1 v ' * p1 w) ').
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L36:
CSNo (p1 v * p1 w ' * p1 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L37:
CSNo (p1 w * p0 z * p0 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L38:
CSNo (p1 w * p0 v ' * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L39:
CSNo (p1 z * p1 v * p1 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L40:
CSNo (p0 z * p1 v ' * p1 w).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L41:
CSNo (p0 v * p1 w ' * p1 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L42:
CSNo (- p1 v * p1 w ' * p1 z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L43:
CSNo (p1 z * p0 w ' * p0 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L44:
CSNo (p1 z * p0 v ' * p0 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L45:
CSNo (- p1 z * p1 v * p1 w ').
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L46:
CSNo (- p0 z * p1 v ' * p1 w).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L47:
CSNo (p0 w ' * p1 v ' * p1 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L48:
CSNo (- p0 v * p1 w ' * p1 z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L49:
CSNo (- p0 w ' * p1 v ' * p1 z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L50:
CSNo (p1 w * p0 z + p1 z * p0 w ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L51:
CSNo (p1 v * p0 w + p1 w * p0 v ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L52:
CSNo (p0 z * p0 w + - p1 w ' * p1 z).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L53:
CSNo (p0 w * p0 v + - p1 v ' * p1 w).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L54:
CSNo ((p1 v * p0 w + p1 w * p0 v ') ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L55:
CSNo ((p0 w * p0 v + - p1 v ' * p1 w) ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L56:
CSNo (p0 w ' * p1 v ' + p0 v ' ' * p1 w).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L57:
CSNo ((p1 v * p0 w) ' + (p1 w * p0 v ') ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L58:
CSNo ((p1 v * p0 w + p1 w * p0 v ') * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L59:
CSNo (p0 v ' * p0 w ' + - (p1 v ' * p1 w) ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L60:
CSNo ((p0 w * p0 v) ' + (- p1 v ' * p1 w) ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L61:
CSNo (p1 v * (p0 z * p0 w + - p1 w ' * p1 z)).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L62:
CSNo ((p1 w * p0 z + p1 z * p0 w ') * p0 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L63:
CSNo (p0 z * (p0 w * p0 v + - p1 v ' * p1 w)).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L64:
CSNo ((p1 v * p0 w + p1 w * p0 v ') ' * p1 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L65:
CSNo (p1 z * (p0 w * p0 v + - p1 v ' * p1 w) ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L66:
CSNo (- (p1 v * p0 w + p1 w * p0 v ') ' * p1 z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L67:
CSNo (p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L68:
CSNo (p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L69:
CSNo (- p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L70:
CSNo (- p1 v * p1 w ' * p1 z + p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L71:
CSNo (p1 w * p0 v ' * p0 z + p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L72:
CSNo (- p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L73:
CSNo (p1 v * (p0 z * p0 w + - p1 w ' * p1 z) + (p1 w * p0 z + p1 z * p0 w ') * p0 v ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L74:
CSNo ((p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 w * p0 v + - p1 v ' * p1 w) ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L75:
CSNo (p0 z * (p0 w * p0 v + - p1 v ' * p1 w) + - (p1 v * p0 w + p1 w * p0 v ') ' * p1 z).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L76:
CSNo (p1 v * p0 z * p0 w + - p1 v * p1 w ' * p1 z + p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L77:
CSNo (p1 v * p0 w * p0 z + p1 w * p0 v ' * p0 z + p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L78:
CSNo (p0 z * p0 w * p0 v + - p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L79:
CSNo (p0 v * p1 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L80:
CSNo (p1 z * p0 v).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L81:
CSNo (p1 w ' * p1 z * p0 v).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L82:
CSNo (- p1 w ' * p1 z * p0 v).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L83:
CSNo (p1 v ' * p1 w * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L84:
CSNo (p1 v ' * p1 z * p0 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L85:
CSNo (- p1 v ' * p1 w * p0 z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L86:
CSNo (- p1 v ' * p1 z * p0 w ').
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L87:
CSNo (- p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L88:
CSNo (- p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L89:
CSNo (- p1 v ').
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim L90:
CSNo (- p1 v * p1 w ').
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We will prove p0 (mult' z (mult' w v)) = p0 (mult' (mult' z w) v).
Use transitivity with
p0 z * p0 (mult' w v) + - p1 (mult' w v) ' * p1 z,
p0 z * (p0 w * p0 v + - p1 v ' * p1 w) + - (p1 v * p0 w + p1 w * p0 v ') ' * p1 z,
p0 z * p0 w * p0 v + - p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z,
p0 z * p0 w * p0 v + - p1 w ' * p1 z * p0 v + - p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w ',
(p0 z * p0 w + - p1 w ' * p1 z) * p0 v + - p1 v ' * (p1 w * p0 z + p1 z * p0 w '), and
p0 (mult' z w) * p0 v + - p1 v ' * p1 (mult' z w).
An
exact proof term for the current goal is
mul_HSNo_proj0 z (mult' w v) Hz Lwv.
We will
prove p0 z * p0 (mult' w v) + - p1 (mult' w v) ' * p1 z = p0 z * (p0 w * p0 v + - p1 v ' * p1 w) + - (p1 v * p0 w + p1 w * p0 v ') ' * p1 z.
Use f_equal.
Use f_equal.
Use f_equal.
Use f_equal.
We will
prove p0 z * (p0 w * p0 v + - p1 v ' * p1 w) + - (p1 v * p0 w + p1 w * p0 v ') ' * p1 z = p0 z * p0 w * p0 v + - p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z.
rewrite the current goal using
add_CSNo_assoc (p0 z * p0 w * p0 v) (- p0 z * p1 v ' * p1 w) (- p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z) ?? ?? ?? (from right to left).
Use f_equal.
We will
prove p0 z * (p0 w * p0 v + - p1 v ' * p1 w) = p0 z * p0 w * p0 v + - p0 z * p1 v ' * p1 w.
rewrite the current goal using
mul_CSNo_distrL (p0 z) (p0 w * p0 v) (- p1 v ' * p1 w) ?? ?? ?? (from left to right).
We will
prove p0 z * p0 w * p0 v + p0 z * (- p1 v ' * p1 w) = p0 z * p0 w * p0 v + - p0 z * p1 v ' * p1 w.
Use f_equal.
We will
prove p0 z * (- p1 v ' * p1 w) = - p0 z * p1 v ' * p1 w.
An
exact proof term for the current goal is
minus_mul_CSNo_distrR (p0 z) (p1 v ' * p1 w) ?? ??.
We will
prove - (p1 v * p0 w + p1 w * p0 v ') ' * p1 z = - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z.
Use transitivity with and
- (p0 w ' * p1 v ' * p1 z + p0 v * p1 w ' * p1 z).
Use f_equal.
We will
prove (p1 v * p0 w + p1 w * p0 v ') ' * p1 z = p0 w ' * p1 v ' * p1 z + p0 v * p1 w ' * p1 z.
Use transitivity with and
(p0 w ' * p1 v ' + p0 v * p1 w ') * p1 z.
Use f_equal.
We will
prove (p1 v * p0 w + p1 w * p0 v ') ' = p0 w ' * p1 v ' + p0 v * p1 w '.
Use transitivity with and
(p1 v * p0 w) ' + (p1 w * p0 v ') '.
An
exact proof term for the current goal is
conj_add_CSNo (p1 v * p0 w) (p1 w * p0 v ') ?? ??.
We will
prove (p1 v * p0 w) ' + (p1 w * p0 v ') ' = p0 w ' * p1 v ' + p0 v * p1 w '.
Use f_equal.
An exact proof term for the current goal is conj_mul_CSNo (p1 v) (p0 w) ?? ??.
rewrite the current goal using
conj_mul_CSNo (p1 w) (p0 v ') ?? ?? (from left to right).
We will
prove p0 v ' ' * p1 w ' = p0 v * p1 w '.
Use f_equal.
An exact proof term for the current goal is conj_CSNo_invol (p0 v) ??.
We will
prove (p0 w ' * p1 v ' + p0 v * p1 w ') * p1 z = p0 w ' * p1 v ' * p1 z + p0 v * p1 w ' * p1 z.
rewrite the current goal using
mul_CSNo_distrR (p0 w ' * p1 v ') (p0 v * p1 w ') (p1 z) ?? ?? ?? (from left to right).
Use f_equal.
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_assoc (p0 w ') (p1 v ') (p1 z) ?? ?? ??.
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_assoc (p0 v) (p1 w ') (p1 z) ?? ?? ??.
We will
prove - (p0 w ' * p1 v ' * p1 z + p0 v * p1 w ' * p1 z) = - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z.
An
exact proof term for the current goal is
minus_add_CSNo (p0 w ' * p1 v ' * p1 z) (p0 v * p1 w ' * p1 z) ?? ??.
We will
prove p0 z * p0 w * p0 v + - p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z = p0 z * p0 w * p0 v + - p1 w ' * p1 z * p0 v + - p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w '.
Use f_equal.
We will
prove - p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z = - p1 w ' * p1 z * p0 v + - p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w '.
We will
prove - p0 v * p1 w ' * p1 z + - p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z = - p1 w ' * p1 z * p0 v + - p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w '.
Use f_equal.
We will
prove - p0 v * p1 w ' * p1 z = - p1 w ' * p1 z * p0 v.
Use f_equal.
Use symmetry.
Use f_equal.
We will
prove - p0 z * p1 v ' * p1 w = - p1 v ' * p1 w * p0 z.
Use f_equal.
Use symmetry.
We will
prove - p0 w ' * p1 v ' * p1 z = - p1 v ' * p1 z * p0 w '.
Use f_equal.
Use symmetry.
We will
prove p0 z * p0 w * p0 v + - p1 w ' * p1 z * p0 v + - p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w ' = (p0 z * p0 w + - p1 w ' * p1 z) * p0 v + - p1 v ' * (p1 w * p0 z + p1 z * p0 w ').
rewrite the current goal using
add_CSNo_assoc (p0 z * p0 w * p0 v) (- p1 w ' * p1 z * p0 v) (- p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w ') ?? ?? ?? (from right to left).
Use f_equal.
We will
prove p0 z * p0 w * p0 v + - p1 w ' * p1 z * p0 v = (p0 z * p0 w + - p1 w ' * p1 z) * p0 v.
rewrite the current goal using mul_CSNo_assoc (p0 z) (p0 w) (p0 v) ?? ?? ?? (from left to right).
We will
prove (p0 z * p0 w) * p0 v + - p1 w ' * p1 z * p0 v = (p0 z * p0 w + - p1 w ' * p1 z) * p0 v.
rewrite the current goal using
mul_CSNo_assoc (p1 w ') (p1 z) (p0 v) ?? ?? ?? (from left to right).
rewrite the current goal using
minus_mul_CSNo_distrL (p1 w ' * p1 z) (p0 v) ?? ?? (from right to left).
We will
prove (p0 z * p0 w) * p0 v + (- p1 w ' * p1 z) * p0 v = (p0 z * p0 w + - p1 w ' * p1 z) * p0 v.
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_distrR (p0 z * p0 w) (- p1 w ' * p1 z) (p0 v) ?? ?? ??.
We will
prove - p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w ' = - p1 v ' * (p1 w * p0 z + p1 z * p0 w ').
rewrite the current goal using
minus_mul_CSNo_distrL (p1 v ') (p1 w * p0 z) ?? ?? (from right to left).
rewrite the current goal using
minus_mul_CSNo_distrL (p1 v ') (p1 z * p0 w ') ?? ?? (from right to left).
rewrite the current goal using
mul_CSNo_distrL (- p1 v ') (p1 w * p0 z) (p1 z * p0 w ') ?? ?? ?? (from right to left).
An
exact proof term for the current goal is
minus_mul_CSNo_distrL (p1 v ') (p1 w * p0 z + p1 z * p0 w ') ?? ??.
We will
prove (p0 z * p0 w + - p1 w ' * p1 z) * p0 v + - p1 v ' * (p1 w * p0 z + p1 z * p0 w ') = p0 (mult' z w) * p0 v + - p1 v ' * p1 (mult' z w).
Use f_equal.
Use f_equal.
Use symmetry.
Use f_equal.
Use f_equal.
Use symmetry.
Use symmetry.
An
exact proof term for the current goal is
mul_HSNo_proj0 (mult' z w) v Lzw Hv.
We will prove p1 (mult' z (mult' w v)) = p1 (mult' (mult' z w) v).
Use transitivity with
p1 (mult' w v) * p0 z + p1 z * p0 (mult' w v) ',
(p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 w * p0 v + - (p1 v ' * p1 w)) ',
(p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 v ' * p0 w ' + - p1 v * p1 w '),
p1 v * p0 w * p0 z + p1 w * p0 v ' * p0 z + p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ',
p1 v * p0 z * p0 w + - p1 v * p1 w ' * p1 z + p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ',
p1 v * (p0 z * p0 w + - p1 w ' * p1 z) + (p1 w * p0 z + p1 z * p0 w ') * p0 v ', and
p1 v * p0 (mult' z w) + p1 (mult' z w) * p0 v '.
An
exact proof term for the current goal is
mul_HSNo_proj1 z (mult' w v) Hz Lwv.
We will
prove p1 (mult' w v) * p0 z + p1 z * p0 (mult' w v) ' = (p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 w * p0 v + - (p1 v ' * p1 w)) '.
Use f_equal.
Use f_equal.
Use f_equal.
We will
prove (p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 w * p0 v + - (p1 v ' * p1 w)) ' = (p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 v ' * p0 w ' + - p1 v * p1 w ').
Use f_equal.
Use f_equal.
We will
prove (p0 w * p0 v + - (p1 v ' * p1 w)) ' = p0 v ' * p0 w ' + - p1 v * p1 w '.
rewrite the current goal using
conj_add_CSNo (p0 w * p0 v) (- (p1 v ' * p1 w)) ?? ?? (from left to right).
rewrite the current goal using
conj_minus_CSNo (p1 v ' * p1 w) ?? (from left to right).
We will
prove (p0 w * p0 v) ' + - (p1 v ' * p1 w) ' = p0 v ' * p0 w ' + - p1 v * p1 w '.
Use f_equal.
An exact proof term for the current goal is conj_mul_CSNo (p0 w) (p0 v) ?? ??.
Use f_equal.
rewrite the current goal using
conj_mul_CSNo (p1 v ') (p1 w) ?? ?? (from left to right).
We will
prove p1 w ' * p1 v ' ' = p1 v * p1 w '.
rewrite the current goal using conj_CSNo_invol (p1 v) ?? (from left to right).
We will
prove p1 w ' * p1 v = p1 v * p1 w '.
An
exact proof term for the current goal is
mul_CSNo_com (p1 w ') (p1 v) ?? ??.
We will
prove (p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 v ' * p0 w ' + - p1 v * p1 w ') = p1 v * p0 w * p0 z + p1 w * p0 v ' * p0 z + p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w '.
rewrite the current goal using
add_CSNo_assoc (p1 v * p0 w * p0 z) (p1 w * p0 v ' * p0 z) (p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ') ?? ?? ?? (from right to left).
Use f_equal.
We will
prove (p1 v * p0 w + p1 w * p0 v ') * p0 z = p1 v * p0 w * p0 z + p1 w * p0 v ' * p0 z.
rewrite the current goal using
mul_CSNo_distrR (p1 v * p0 w) (p1 w * p0 v ') (p0 z) ?? ?? ?? (from left to right).
rewrite the current goal using mul_CSNo_assoc (p1 v) (p0 w) (p0 z) ?? ?? ?? (from left to right).
rewrite the current goal using
mul_CSNo_assoc (p1 w) (p0 v ') (p0 z) ?? ?? ?? (from left to right).
Use reflexivity.
We will
prove p1 z * (p0 v ' * p0 w ' + - p1 v * p1 w ') = p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w '.
rewrite the current goal using
mul_CSNo_distrL (p1 z) (p0 v ' * p0 w ') (- p1 v * p1 w ') ?? ?? ?? (from left to right).
Use f_equal.
We will
prove p1 z * (- p1 v * p1 w ') = - p1 z * p1 v * p1 w '.
An
exact proof term for the current goal is
minus_mul_CSNo_distrR (p1 z) (p1 v * p1 w ') ?? ??.
We will
prove p1 v * p0 w * p0 z + p1 w * p0 v ' * p0 z + p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ' = p1 v * p0 z * p0 w + - p1 v * p1 w ' * p1 z + p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v '.
Use f_equal.
Use f_equal.
An exact proof term for the current goal is mul_CSNo_com (p0 w) (p0 z) ?? ??.
We will
prove p1 w * p0 v ' * p0 z + p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ' = - p1 v * p1 w ' * p1 z + p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v '.
rewrite the current goal using
add_CSNo_rotate_3_1 (p1 w * p0 v ' * p0 z) (p1 z * p0 v ' * p0 w ') (- p1 z * p1 v * p1 w ') ?? ?? ?? (from left to right).
Use f_equal.
We will
prove - p1 z * p1 v * p1 w ' = - p1 v * p1 w ' * p1 z.
Use f_equal.
Use symmetry.
Use f_equal.
We will
prove p1 w * p0 v ' * p0 z = p1 w * p0 z * p0 v '.
Use f_equal.
An
exact proof term for the current goal is
mul_CSNo_com (p0 v ') (p0 z) ?? ??.
We will
prove p1 z * p0 v ' * p0 w ' = p1 z * p0 w ' * p0 v '.
Use f_equal.
An
exact proof term for the current goal is
mul_CSNo_com (p0 v ') (p0 w ') ?? ??.
We will
prove p1 v * p0 z * p0 w + - p1 v * p1 w ' * p1 z + p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ' = p1 v * (p0 z * p0 w + - p1 w ' * p1 z) + (p1 w * p0 z + p1 z * p0 w ') * p0 v '.
rewrite the current goal using
add_CSNo_assoc (p1 v * p0 z * p0 w) (- p1 v * p1 w ' * p1 z) (p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ') ?? ?? ?? (from right to left).
Use f_equal.
We will
prove p1 v * p0 z * p0 w + - p1 v * p1 w ' * p1 z = p1 v * (p0 z * p0 w + - p1 w ' * p1 z).
rewrite the current goal using
mul_CSNo_distrL (p1 v) (p0 z * p0 w) (- p1 w ' * p1 z) ?? ?? ?? (from left to right).
We will
prove p1 v * p0 z * p0 w + - p1 v * p1 w ' * p1 z = p1 v * p0 z * p0 w + p1 v * (- p1 w ' * p1 z).
Use f_equal.
We will
prove - p1 v * p1 w ' * p1 z = p1 v * (- p1 w ' * p1 z).
Use symmetry.
An
exact proof term for the current goal is
minus_mul_CSNo_distrR (p1 v) (p1 w ' * p1 z) ?? ??.
We will
prove p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ' = (p1 w * p0 z + p1 z * p0 w ') * p0 v '.
rewrite the current goal using
mul_CSNo_assoc (p1 w) (p0 z) (p0 v ') ?? ?? ?? (from left to right).
rewrite the current goal using
mul_CSNo_assoc (p1 z) (p0 w ') (p0 v ') ?? ?? ?? (from left to right).
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_distrR (p1 w * p0 z) (p1 z * p0 w ') (p0 v ') ?? ?? ??.
We will
prove p1 v * (p0 z * p0 w + - p1 w ' * p1 z) + (p1 w * p0 z + p1 z * p0 w ') * p0 v ' = p1 v * p0 (mult' z w) + p1 (mult' z w) * p0 v '.
Use f_equal.
Use f_equal.
Use symmetry.
Use f_equal.
Use symmetry.
Use symmetry.
We will
prove p1 (mult' (mult' z w) v) = p1 v * p0 (mult' z w) + p1 (mult' z w) * p0 v '.
An
exact proof term for the current goal is
mul_HSNo_proj1 (mult' z w) v Lzw Hv.