proposition: Lemma k_related_spec {k k' : nat} (G : subgraph k k') : forall x y, k_related k k' G x y <-> (forall f : fin k, match G f with | Some (weight, d) => if weight then k_tuple_val f x < k_tuple_val d y else Peano.le (k_tuple_val f x) (k_tuple_val d y) | None => False end).
proof: Proof. eapply k_related_elim. split; auto. intros []. intros f. depelim f. intros n k'' g b f. intros H. intros gz [x rx] y. specialize (H (x, rx) y rx y). simpl. rewrite H. clear H. split. + intros [xlt relr]. intros f'. depelim f'. rewrite gz. apply xlt. apply relr. + intros Hf. split. specialize (Hf fz). rewrite gz in Hf. apply Hf. intros f'. apply Hf. + intros n k'' g gf x y. split. intros []. intros f. specialize (f fz). now rewrite gf in f. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect