proposition: Lemma mult_INC : forall n m:nat, INC (n * m) = INC n * INC m.
proof: Proof. intros n m; induction n. intuition (auto with complex). rewrite S_INC. simpl (S n * m)%nat. rewrite add_INC. rewrite IHn. ring. Qed.
imports: Ctacfield Cbase Cpow Lia