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