proposition: Lemma add_INC : forall n m:nat, INC (n + m) = INC n + INC m.
proof: Proof. intros n m. induction n ; auto with complex. rewrite S_INC ; rewrite Cadd_assoc ; rewrite Cadd_comm ; rewrite Cadd_assoc. rewrite Cadd_comm in IHn ; rewrite <- IHn. replace (S n + m)%nat with (S (n + m)) by (simpl ; reflexivity). rewrite S_INC ; auto with complex. Qed.
imports: Ctacfield Cbase Cpow Lia