proposition: Lemma to_plus2_strext:fun_strext (S1:=nat_as_CSetoid) (S2:=FS_as_CSetoid nat_as_CSetoid (FS_as_CSetoid nat_as_CSetoid nat_as_CSetoid)) (fun m : nat => plus2 m).
proof: Proof. unfold fun_strext. intros x y. simpl. unfold ap_fun. simpl. intro H. elim H. clear H. unfold ap_fun. intros a H. elim H. clear H. intros a0 H. unfold plus1 in H. simpl in H. set (H1:= (plus_strext)). unfold bin_fun_strext in H1. cut (((x+a){#N}(y+a)) or (a0 {#N} a0)). intro H2. elim H2. clear H2. intro H2. set (H3:=(H1 x y a a H2)). simpl in H3. elim H3. clear H3. intro H3. exact H3. clear H3. intro H3. set (H5:=(ap_nat_irreflexive a)). set (H7:= (H5 H3)). contradiction. set (H5:=(ap_nat_irreflexive a0)). intro H6. set (H7:= (H5 H6)). contradiction. apply H1. exact H. Qed.
imports: CoRN.model.structures.Nsec CoRN.algebra.CSetoidFun