proposition: Lemma valid_le_compat : forall k l p, valid k p -> (k <= l)%positive -> valid l p.
proof: Proof. intros k l p H Hl; induction H; constructor; eauto. now eapply Pos.lt_le_trans; eassumption. Qed.
imports: Bool PArith DecidableClass Ring Lia