proposition: Lemma not_INC : forall n m:nat, n <> m -> INC n <> INC m.
proof: Proof. induction n; induction m. intuition. revert m IHm. intros n1 H1 H2. intro H. apply H2. rewrite S_INC in H. generalize (Cre_INC_pos n1). intro H3. destruct (INC n1). simpl in *. apply Ceq in H. elim H. intros H5 H6. simpl in *. lra. revert n IHn. intros n1 H1 H2. intro H. apply H2. rewrite S_INC in H. generalize (Cre_INC_pos n1). intro H3. destruct (INC n1). simpl in *. apply Ceq in H. elim H. intros H5 H6. simpl in *. lra. revert n IHn m IHm. intros n1 H3 n0 H1 H4. do 2 rewrite S_INC. assert ( H : (INC n1 <> INC n0 -> INC n1 + C1 <> INC n0 + C1)). intros temp1 temp2. apply Cadd_eq_reg_r in temp2. apply temp1. exact temp2. apply H. apply H3. intuition. Qed.
imports: Ctacfield Cbase Cpow Lia