proposition: Lemma nexp_strong_ext : forall n, fun_strext (nexp n).
proof: Proof. intro n; red in |- *; induction n as [| n Hrecn]; simpl in |- *; intros x y H. Proof. elim (ap_irreflexive _ _ H). elim (cs_bin_op_strext _ cr_mult _ _ _ _ H); auto. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CSums CoRN.algebra.CAbMonoids Coq.Sorting.Permutation CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq(Lia)