Example of a setoid: Q+
Setoid
We will examine the subsetoid of positive rationals of the setoid of rational numbers.
Lemma ap_Qpos_irreflexive1 : irreflexive (A:=Qpos) Qap.
Lemma ap_Qpos_symmetric1 : Csymmetric (A:=Qpos) Qap.
Lemma ap_Qpos_cotransitive1 : cotransitive (A:=Qpos) Qap.
Lemma ap_Qpos_tight1 : tight_apart (A:=Qpos) Qeq Qap.
Definition ap_Qpos_is_apartness := Build_is_CSetoid _ _ _
ap_Qpos_irreflexive1 ap_Qpos_symmetric1 ap_Qpos_cotransitive1 ap_Qpos_tight1.
Definition Qpos_as_CSetoid := Build_CSetoid _ _ _ ap_Qpos_is_apartness.
Canonical Structure Qpos_as_CSetoid.
Canonical Structure Qpos_as_Setoid := (cs_crr Qpos_as_CSetoid).
Lemma Qpos_plus_strext : bin_fun_strext Qpos_as_CSetoid Qpos_as_CSetoid Qpos_as_CSetoid Qpos_plus.
Definition Qpos_plus_is_bin_fun := Build_CSetoid_bin_fun _ _ _ _ Qpos_plus_strext.
Canonical Structure Qpos_plus_is_bin_fun.
Lemma associative_Qpos_plus : associative Qpos_plus.
Lemma ap_Qpos_symmetric1 : Csymmetric (A:=Qpos) Qap.
Lemma ap_Qpos_cotransitive1 : cotransitive (A:=Qpos) Qap.
Lemma ap_Qpos_tight1 : tight_apart (A:=Qpos) Qeq Qap.
Definition ap_Qpos_is_apartness := Build_is_CSetoid _ _ _
ap_Qpos_irreflexive1 ap_Qpos_symmetric1 ap_Qpos_cotransitive1 ap_Qpos_tight1.
Definition Qpos_as_CSetoid := Build_CSetoid _ _ _ ap_Qpos_is_apartness.
Canonical Structure Qpos_as_CSetoid.
Canonical Structure Qpos_as_Setoid := (cs_crr Qpos_as_CSetoid).
Lemma Qpos_plus_strext : bin_fun_strext Qpos_as_CSetoid Qpos_as_CSetoid Qpos_as_CSetoid Qpos_plus.
Definition Qpos_plus_is_bin_fun := Build_CSetoid_bin_fun _ _ _ _ Qpos_plus_strext.
Canonical Structure Qpos_plus_is_bin_fun.
Lemma associative_Qpos_plus : associative Qpos_plus.
Lemma Qpos_mult_strext : bin_op_strext Qpos_as_CSetoid Qpos_mult.
Definition Qpos_mult_is_bin_fun : CSetoid_bin_op Qpos_as_CSetoid := Build_CSetoid_bin_fun _ _ _ _ Qpos_mult_strext.
Canonical Structure Qpos_mult_is_bin_fun.
Lemma associative_Qpos_mult : associative Qpos_mult.
Lemma Qpos_inv_strext : fun_strext Qpos_inv.
Definition Qpos_inv_op := Build_CSetoid_un_op _ _ Qpos_inv_strext.
Canonical Structure Qpos_inv_op.
Definition Qpos_div2 := projected_bin_fun _ _ _ Qpos_mult_is_bin_fun (Qpos_inv_op (2#1)%Qpos).
Definition multdiv2 := compose_CSetoid_un_bin_fun _ _ _ Qpos_mult_is_bin_fun Qpos_div2.
Lemma associative_multdiv2 : associative multdiv2.
And its inverse multdiv4: x ↦ 4/x.
Definition mult4 := projected_bin_fun _ _ _ Qpos_mult_is_bin_fun (4#1)%Qpos.
Definition divmult4 := compose_CSetoid_fun _ _ _ Qpos_inv_op mult4.