proposition: Lemma mat_order_strict_wf : forall dim, well_founded (mat_order_strict dim).
proof: Proof. destruct dim as [|dim]. simpl. apply lt_wf. simpl. intros [a [l [c m]]]. revert l c m. pattern a. apply well_founded_ind with (1:=lt_wf). clear a. intros a1 IHa1 l1 c1 m1. constructor. intros [a2 [l2 [c2 m2]]] [H1 _]. apply IHa1 ; assumption. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)