proposition: Lemma fact_correct : PRcorrect fact Coq.Arith.Factorial.fact.
proof: Proof. intro n; assert (fact_eqn1: forall n, PReval fact (S n) = PReval mult (PReval fact n) (S n)) by reflexivity. induction n as [| n IHn]. - reflexivity. - rewrite fact_eqn1, mult_correct, IHn; cbn; ring. Qed.
imports: Coq(Arith ArithRing List Vector Utf8) hydras(primRec cPair)