proposition: Lemma CForall_map {A B} (P: B -> Type) (f: A -> B) (l: list A): CForall P (map f l) IFF CForall (fun x => P (f x)) l.
proof: Proof. induction l; firstorder. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)