proposition: Fact smono_upto_injective n f : (forall i j, i < j < n -> f i < f j) -> (forall i j, i < n -> j < n -> f i = f j -> i = j).
proof: Proof. intros Hf i j Hi Hj E. destruct (lt_eq_lt_dec i j) as [ [H|] | H ]; auto. + generalize (@Hf i j); intros; lia. + generalize (@Hf j i); intros; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)