proposition: Lemma exist_lt_pi : forall n dim H1 H2, exist (fun n1 => n1 < dim) n H1 = exist (fun n1 => n1 < dim) n H2.
proof: Proof. intros n dim H1 H2. rewrite exist_pi with (a:=n) (P:=fun n1 => n1 < dim) (H2:=H2). reflexivity. intros. apply lt_pi. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)