proposition: Lemma L3 n p : alpha = FS n -> beta = FS p -> P beta.
proof: Proof. intros; subst; red; intros; split. - apply (mult_nf_fin (S p) H). - intros _ gamma H1; destruct (LT_of_finite H1 ). + subst; rewrite mult_a_0; eauto with T1. + destruct H0 as [p0 [H2 H3]]; subst; simpl. apply LT3; eauto with T1. apply Nat.add_lt_le_mono;auto. apply PeanoNat.Nat.mul_le_mono_l; abstract 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)