proposition: Lemma minus_INC : forall n m:nat, (m <= n)%nat -> INC (n - m) = INC n - INC m.
proof: Proof. intros n m H1. induction m. simpl. replace (n-0)%nat with n by intuition (auto with arith). auto with complex. destruct n. inversion H1. replace (S n - S m)%nat with (n - m)%nat by intuition. do 2 rewrite S_INC. replace (INC n + C1 - (INC m + C1)) with (INC n - INC m) by ring. replace (INC (S n) - INC m) with (C1 + INC n - INC m) in IHm. replace (INC (S n - m)) with (C1 + INC (n - m)) in IHm. assert ( H :( C1 + INC (n - m) = C1 + INC n - INC m) -> (INC (n - m) = INC n - INC m)). unfold Cminus ; rewrite Cadd_assoc ; apply (Cadd_eq_reg_l C1). apply H. apply IHm. intuition (auto with arith). replace (S n - m)%nat with (S (n - m))%nat. rewrite S_INC. auto with complex. intuition (auto with arith). rewrite S_INC. ring. Qed.
imports: Ctacfield Cbase Cpow Lia