proposition: Lemma power_Dlt_compat : forall x y n, Dlt x y -> Dlt (inj (pos_power_val x (S n))) (inj (pos_power_val y (S n))).
proof: Proof. intros x y. destruct x. destruct y. unfold Dlt. simpl. induction n; simpl; intros. lia. ded (IHn H). apply Z.le_lt_trans with (m := x * (x0 * power x0 n)). apply Zmult_le_compat_l. lia. hyp. apply Zmult_gt_0_lt_compat_r. apply Z.lt_gt. apply Zmult_lt_O_compat. lia. apply spos_power. lia. hyp. Qed.
imports: CoLoR(LogicUtil) Coq(Lia) CoLoR(RelUtil) Coq(Zwf Wellfounded) CoLoR(SN)