mutual
    *-distribʳ : ∀ {n} (x y z : BitVector n) → (y + z) * x ≡ (y * x) + (z * x)
    *-distribʳ [] [] [] = refl
    *-distribʳ {Nsuc n} xs ys zs = *-distribʳ1 xs ys zs

    *-distribʳ1 : ∀ {n} (x y z : BitVector (Nsuc n)) → (y + z) * x ≡ (y * x) + (z * x)
    *-distribʳ1 xs (0# ∷ ys) (0# ∷ zs) rewrite *-distribʳ (droplast xs) ys zs = refl
    *-distribʳ1 (0# ∷ xs) (0# ∷ ys) (1# ∷ zs)
             rewrite *-distribʳ (droplast (0# ∷ xs)) ys zs
                   | sym (assoc xs (ys * droplast (0# ∷ xs)) (zs * droplast (0# ∷ xs)))
                   | comm xs (ys * droplast (0# ∷ xs))
                   | assoc (ys * droplast (0# ∷ xs)) xs (zs * droplast (0# ∷ xs)) = refl
    *-distribʳ1 (1# ∷ xs) (0# ∷ ys) (1# ∷ zs)
             rewrite *-distribʳ (droplast (1# ∷ xs)) ys zs
                   | sym (assoc xs (ys * droplast (1# ∷ xs)) (zs * droplast (1# ∷ xs)))
                   | comm xs (ys * droplast (1# ∷ xs))
                   | assoc (ys * droplast (1# ∷ xs)) xs (zs * droplast (1# ∷ xs)) = refl
    *-distribʳ1 (0# ∷ xs) (1# ∷ ys) (0# ∷ zs)
             rewrite *-distribʳ (droplast (0# ∷ xs)) ys zs
                   | assoc xs (ys * droplast (0# ∷ xs)) (zs * droplast (0# ∷ xs)) = refl
    *-distribʳ1 (1# ∷ xs) (1# ∷ ys) (0# ∷ zs)
             rewrite *-distribʳ (droplast (1# ∷ xs)) ys zs
                   | assoc xs (ys * droplast (1# ∷ xs)) (zs * droplast (1# ∷ xs)) = refl
    *-distribʳ1 (0# ∷ xs) (1# ∷ ys) (1# ∷ zs) rewrite extract-carry ys zs 
                                                    | *-distribʳ (droplast (0# ∷ xs)) (one _) (add′ 0# ys zs) 
                                                    | *-distribʳ (droplast (0# ∷ xs)) ys zs 
                                                    | assoc xs (ys * droplast (0# ∷ xs)) (xs + (zs * droplast (0# ∷ xs)))
                                                    | sym (assoc (ys * droplast (0# ∷ xs)) xs (zs * droplast (0# ∷ xs)))
                                                    | comm (ys * droplast (0# ∷ xs)) xs 
                                                    | assoc xs (ys * droplast (0# ∷ xs)) (zs * droplast (0# ∷ xs))
                                                    | sym (assoc xs xs ((ys * droplast (0# ∷ xs)) + (zs * droplast (0# ∷ xs))))
                                                    | *-identityˡ (droplast (0# ∷ xs))
                                                    | shift-to-add 0# xs
                                                    = refl
    *-distribʳ1 (1# ∷ xs) (1# ∷ ys) (1# ∷ zs) = cong (_∷_ 0#) {!!}