proposition: Fact sinc_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. Proof using Hq Hr. intros Hf i j Hi Hj E. destruct (lt_eq_lt_dec i j) as [ [] | ]; auto. + generalize (Hf i j); intros; lia. + generalize (Hf j i); intros; lia. Qed.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)