proposition: Theorem plus_assoc (x y z : No) : (x + y) + z = x + (y + z).
proof: Proof. one_line_proof (equiv_sum_assoc _ _ _) (equiv_sum_assoc _ _ _); one_line_proof 1%equiv 1%equiv. Defined.
imports: HoTT.Basics HoTT.Types HoTT.Spaces.No.Core HoTT.Spaces.No.Negation