proposition: Lemma mult_fin_rw alpha (i:nat) : alpha * i = Mult_i alpha i.
proof: Proof. orefl; cbn; f_equal; now destruct i. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)