proposition: Lemma succ_of_plus_finite : forall a (H: nf a) (i:nat) , succ (a + i) = a + S i.
proof: Proof. induction a; cbn. - destruct i; reflexivity. - destruct i. + simpl. destruct a1. * simpl; replace (n + 0)%nat with n. { auto. } { abstract lia. } * simpl; rewrite succ_is_plus_one; auto. + simpl; destruct a1. * simpl; replace (S (n + i)) with (n + S i)%nat; auto. * simpl; assert (nf a2) by eauto with T1. generalize (IHa2 H0 (S i)). replace (T1nat (S i)) with (FS i); auto. replace (T1nat (S (S i))) with (FS (S i)). { intro H1; now rewrite H1. } reflexivity. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)