Fix inner product space laws

[langston-barrett]

One needs the additional axioms, see #15.

   ; in_pos_def1    :> ∀ v, PropHolds (0 ≤ ⟨v,v⟩)
   ; in_pos_def2    :> ∀ v, 0 = ⟨v,v⟩ <-> v = mon_unit
   ; inprod_proper :> Proper ((=) ==> (=) ==> (=)) (⟨⟩)