Record VSpace (F : CField) : Type :=
{vs_vs :> CGroup;
vs_op : CSetoid_outer_op F vs_vs;
vs_assoc : forall a b v, vs_op (a[*]b) v [=] vs_op a (vs_op b v);
vs_unit : forall v, vs_op 1 v [=] v;
vs_distl : forall a b v, vs_op (a[+]b) v [=] vs_op a v[+]vs_op b v;
vs_distr : forall a v u, vs_op a (v[+]u) [=] vs_op a v[+]vs_op a u}.
Infix "'" := vs_op (at level 30, no associativity).
Let F be a fiels and let V be a vector space over F
Section VS_basics.
Variable F : CField.
Variable V : VSpace F.
Lemma vs_op_zero : forall a : F, a['] (0:V) [=] 0.
Lemma zero_vs_op : forall v : V, 0[']v [=] 0.
Lemma vs_op_inv_V : forall (x : F) (y : V), x['][--]y [=] [--] (x[']y).
Lemma vs_op_inv_S : forall (x : F) (y : V), [--]x[']y [=] [--] (x[']y).
Lemma vs_inv_assoc : forall (a : F) a_ (v : V), v [=] f_rcpcl a a_['] (a[']v).
Lemma ap_zero_vs_op_l : forall (a : F) (v : V), a[']v [#] 0 -> a [#] 0.
Lemma ap_zero_vs_op_r : forall (a : F) (v : V), a[']v [#] 0 -> v [#] 0.
Lemma vs_op_resp_ap_rht : forall (a : F) (v u : V), a [#] 0 -> v [#] u -> a[']v [#] a[']u.
Lemma vs_op_resp_ap_zero : forall (a : F) (v : V), a [#] 0 -> v [#] 0 -> a[']v [#] 0.
Lemma vs_op_resp_ap_lft : forall (a b : F) (v : V), a [#] b -> v [#] 0 -> a[']v [#] b[']v.
End VS_basics.