proposition: Lemma Zopp_strext : fun_strext (S1:=Z_as_CSetoid) (S2:=Z_as_CSetoid) Z.opp.
proof: Proof. red in |- *. simpl in |- *. unfold ap_Z in |- *. intros x y H. intro H0. apply H. exact (f_equal Z.opp H0). Qed.
imports: CoRN.model.structures.Zsec CoRN.algebra.CSetoidFun