proof(SafeAngle): DISCHARGE fromTo{Degrees,Radians}Roundtrip via Refl (proven#90) (#106)

Tenth "overly cautious OWED" discharge of today's [proven#90 Phase
3](#90) campaign.

## What it does

\`\`\`idris
public export
fromToDegreesRoundtrip : (d : Double) -> toDegrees (fromDegrees d) = d
fromToDegreesRoundtrip _ = Refl

public export
fromToRadiansRoundtrip : (r : Double) -> toRadians (fromRadians r) = r
fromToRadiansRoundtrip _ = Refl
\`\`\`

## Why it works

Both proofs are unit-constructor pattern matches with no Double
arithmetic:
- \`fromDegrees d = MkAngle d Degrees\` (SafeAngle.idr L108-110)
- \`toDegrees (MkAngle v Degrees) = v\` (first clause, L86)
- Composition reduces by Refl

The OWED's "Double-comparison opacity" blocker applies only to attempts
to REDUCE \`d ?= d'\` for two different Doubles. Here the value passes
through unchanged via constructor reduction; no Double arithmetic or
comparison enters the proof.

Refs #90

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/Proven/SafeAngle/Proofs.idr

@@ -217,15 +217,20 @@ angleDifferenceIsRadians a b = Refl
 -- the residual debt is visible.
 --------------------------------------------------------------------------------
 
-||| OWED: `fromDegrees` round-trips through `toDegrees`. Blocked on
-||| the absence of a numerical-equivalence tactic for `Double` literals
-||| in Idris2 0.8.0.
+||| DISCHARGED: `fromDegrees` round-trips through `toDegrees`.
+||| `fromDegrees d = MkAngle d Degrees` (SafeAngle.idr L108-110)
+||| then `toDegrees (MkAngle v Degrees) = v` (first clause, L86).
+||| No Double arithmetic enters — the `Degrees` unit constructor
+||| pattern-matches and the value passes through unchanged.
 public export
-0 fromToDegreesRoundtrip :
+fromToDegreesRoundtrip :
   (d : Double) -> toDegrees (fromDegrees d) = d
+fromToDegreesRoundtrip _ = Refl
 
-||| OWED: `fromRadians` round-trips through `toRadians`. Same blocker
-||| as `fromToDegreesRoundtrip`.
+||| DISCHARGED: `fromRadians` round-trips through `toRadians`. Same
+||| structure as `fromToDegreesRoundtrip` — `fromRadians r = MkAngle r
+||| Radians` then `toRadians (MkAngle v Radians) = v` (first clause).
 public export
-0 fromToRadiansRoundtrip :
+fromToRadiansRoundtrip :
   (r : Double) -> toRadians (fromRadians r) = r
+fromToRadiansRoundtrip _ = Refl