proposition: Lemma mult_Sn_add (alpha : T1) n : nf alpha -> alpha * (FS (S n)) = alpha * FS n + alpha.
proof: Proof. intro; simpl; destruct alpha. - now simpl. - destruct alpha1. + assert (H0 :alpha2 = zero). { eapply nf_of_finite; eauto. } subst; rewrite plus_compat; f_equal; ring. + simpl; repeat rewrite compare_refl. f_equal; lia. 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)