proposition: Lemma apply x: (N ! ' x) [=] applied x.
proof: Proof. unfold N, applied, an, an_applied. rewrite cm_Sum_apply, map_map. apply (@cm_Sum_eq CRasCMonoid). intro. autorewrite with apply. apply mult_wd. reflexivity. rewrite inject_Q_product. rewrite cr_Product_apply. do 2 rewrite map_map. apply (@cm_Sum_eq (Build_multCMonoid CRasCRing)). intro. unfold Basics.compose. rewrite <- CRminus_Qminus. change ((' (- fst x1)%Q + ' x * (1 + ' x * 0)) == (' x - ' fst x1)). ring. Qed.
imports: CoRN.model.totalorder.QposMinMax Unicode.Utf8 Setoid Arith List Program Permutation metric2.Classified CSetoids CPoly_ApZero CPoly_Degree CRArith CRArith_alg Qmetric Qring CReals Ranges stdlib_omissions.Pair stdlib_omissions.Q list_separates SetoidPermutation CRings