proposition: Lemma S_O_add_INC : forall n:nat, INC (1 + n) = INC 1 + INC n.
proof: Proof. destruct n . auto with complex. replace (1 + S n)%nat with (S (S n))%nat by (simpl ; reflexivity). do 3 (rewrite S_INC) ; replace (INC 0%nat) with C0 by (simpl ; reflexivity). rewrite Cadd_0_l. ring. Qed.
imports: Ctacfield Cbase Cpow Lia